Theory MTF2_Effects

theory MTF2_Effects
imports Move_to_Front
(*  Title:       Effects of the function mtf2 on index and before_in
    Author:      Max Haslbeck
*)

section "Effect of mtf2"

theory MTF2_Effects
imports Move_to_Front
begin



lemma difind_difelem: 
       "i < length xs ⟹ distinct xs ⟹ xs ! j = a ⟹ j < length xs ⟹ i ≠ j 
          ⟹ ~ a = xs ! i"
apply(rule ccontr) by(metis index_nth_id)


lemma fullchar: assumes  "index xs q < length xs"
  shows 
    "(i < length xs) =
  (index xs q < i ∧ i < length xs
    ∨ index xs q = i
    ∨ index xs q - n ≤ i ∧ i < index xs q
    ∨ i < index xs q - n)"
using assms by auto

lemma mtf2_effect:
    "q ∈ set xs ⟹ distinct xs ⟹ (index xs q < i ∧ i < length xs ⟶( index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index xs q < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) < length xs))
    ∧ (index xs q = i ⟶ (index (mtf2 n q xs) (xs!i) = index xs q - n ∧ index (mtf2 n q xs) (xs!i) = index xs q - n))
    ∧ (index xs q - n ≤ i ∧ i < index xs q ⟶ (index (mtf2 n q xs) (xs!i) = Suc (index xs (xs!i)) ∧ index xs q - n < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) ≤ index xs q))
    ∧ (i < index xs q - n ⟶ (index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index (mtf2 n q xs) (xs!i) < index xs q - n))"
unfolding mtf2_def
apply (induct n)
proof -
  case (Suc n)
  note indH=Suc(1)[OF Suc(2) Suc(3), simplified Suc(2) if_True] 
  note qinxs=Suc(2)[simp]
  note distxs=Suc(3)[simp]
  show ?case (is ?toshow)
  apply(simp only: qinxs if_True)
  proof (cases "index xs q ≥ Suc n")
    case True 
    note True1=this
from True have onemore: "[index xs q - Suc n..<index xs q] = (index xs q - Suc n) # [index xs q - n..<index xs q]"
              using Suc_diff_Suc upt_rec by auto

        from onemore have yeah: "swaps [index xs q - Suc n..<index xs q] xs
            = swap (index xs q - Suc n) (swaps  [index xs q - n..<index xs q] xs)" by auto

      have sis: "Suc (index xs q - Suc n) = index xs q - n" using True Suc_diff_Suc by auto
      
      have indq: "index xs q < length xs"
        apply(rule index_less) by auto
 
      let ?i' = "index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i)"
      let ?x = "(xs!i)" and  ?xs="(swaps  [index xs q - n..<index xs q] xs)"
              and ?n="(index xs q - Suc n)"
      have "?i'
          =  index (swap (index xs q - Suc n) (swaps  [index xs q - n..<index xs q] xs)) (xs!i)" using yeah by auto
      also have "… = (if ?x = ?xs ! ?n then Suc ?n else if ?x = ?xs ! Suc ?n then ?n else index ?xs ?x)"
        apply(rule index_swap_distinct)
          apply(simp)
          apply(simp add: sis) using indq by linarith
      finally have i': "?i' = (if ?x = ?xs ! ?n then Suc ?n else if ?x = ?xs ! Suc ?n then ?n else index ?xs ?x)" .
      
      let ?i''="index (swaps [index xs q - n..<index xs q] xs) (xs ! i)"


    show "(index xs q < i ∧ i < length xs ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
     index xs q < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < length xs) ∧
    (index xs q = i ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n) ∧
    (index xs q - Suc n ≤ i ∧ i < index xs q ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = Suc (index xs (xs ! i)) ∧
     index xs q - Suc n < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ≤ index xs q) ∧
    (i < index xs q - Suc n ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < index xs q - Suc n)"
    apply(intro conjI)
    apply(intro impI) apply(elim conjE) prefer 4 apply(intro impI)  prefer 4 apply(intro impI) apply(elim conjE) 
      prefer 4 apply(intro impI) prefer 4
    proof (goal_cases)
      case 1 
      have indH1: "(index xs q < i ∧ i < length xs ⟶
                      ?i'' =  index xs (xs ! i))" using indH by auto
      assume ass: "index xs q < i" and ass2:"i < length xs"      
      then have a: "?i'' =  index xs (xs ! i)" using indH1 by auto
      also have a': "… = i" apply(rule index_nth_id) using ass2 by(auto)
      finally have ii: "?i'' = i" .
      have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
        using indq apply (simp add: less_imp_diff_less)
        apply(simp)
        apply(rule nth_index) apply(simp) using ass2 apply(simp)
        apply(rule index_less) 
          apply(simp) using ass2 apply(simp)
          apply(simp)
        using ii ass by auto
      have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
        using indq True apply (simp add: Suc_diff_Suc less_imp_diff_less)
        apply(simp)
        apply(rule nth_index) apply(simp) using ass2 apply(simp)
        apply(rule index_less) 
          apply(simp) using ass2 apply(simp)
          apply(simp)
        using ii ass Suc_diff_Suc True by auto     
        
      have "?i' = index xs (xs ! i)" unfolding i' using fstF sndF a by simp
      then show ?case using a' ass ass2 by auto
    next
      case 2
      have indH2: "index xs q = i ⟶ ?i'' = index xs (xs ! i) - n" using indH by auto
      assume "index xs q = i"
      then have ass: "i = index xs q" by auto
      with indH2 have a: "i - n = ?i''" by auto
      from ass have c: "index xs (xs ! i) = i" by auto  
      have "Suc (index xs q - Suc n) = i - n" using ass True Suc_diff_Suc by auto
      also have "… = ?i''" using a by auto
      finally have a: "Suc ?n = ?i''" .

      have sndTrue: "?x = ?xs ! Suc ?n" apply(simp add: a)
              apply(rule nth_index[symmetric]) by (simp add: ass)
      have fstFalse: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
        using indq True apply (simp add: Suc_diff_Suc less_imp_diff_less)
        apply(simp)
        apply(rule nth_index) apply(simp) using ass  apply(simp)
        apply(rule index_less) 
          apply(simp) using ass  apply(simp)
          apply(simp)
        using a by auto    

      have "?i' = index xs (xs ! index xs q) - Suc n"
          unfolding i' using sndTrue fstFalse by simp
      with ass show ?case by auto
    next
      case 3
      have indH3: "index xs q - n ≤ i ∧ i < index xs q
              ⟶  ?i'' = Suc (index xs (xs ! i))" using indH by auto
      assume ass: "index xs q - Suc n ≤ i" and
              ass2: "i < index xs q" 
      from ass2 have ilen: "i < length xs" using indq dual_order.strict_trans by blast
      show ?case 
      proof (cases "index xs q - n ≤ i")
        case False
        then have "i < index xs q - n" by auto
        moreover have "(i < index xs q - n ⟶ ?i'' = index xs (xs ! i))" using indH by auto
        ultimately have d: "?i'' = index xs (xs ! i)" by simp
        from False ass have b: "index xs q - Suc n = i" by auto
        have "index xs q < length xs" apply(rule index_less) by (auto)
        have c: "index xs (xs ! i) = i"
          apply(rule index_nth_id) apply(simp) using indq ass2 using less_trans by blast
        from b c d have f: "?i'' = index xs q - Suc n" by auto
        have fstT: "?xs ! ?n = ?x" 
            apply(simp only: f[symmetric]) apply(rule nth_index)
            by (simp add: ilen)

        have "?i' = Suc (index xs q - Suc n)"
          unfolding i' using fstT by simp
        also have "… = Suc (index xs (xs ! i))" by(simp only: b c)
        finally show ?thesis using c False ass by auto
      next
        case True
        with ass2 indH3 have a: "?i'' = Suc (index xs (xs ! i))" by auto
        have jo: "index xs (xs ! i) = i" apply(rule index_nth_id) using ilen by(auto)
        have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
          using indq apply (simp add: less_imp_diff_less)
          apply(simp)
          apply(rule nth_index) apply(simp) using ilen apply(simp)
          apply(rule index_less) 
            apply(simp) using ilen apply(simp)
            apply(simp)
          apply(simp only: a jo) using True by auto
        have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
          using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
          apply(simp)
          apply(rule nth_index) apply(simp) using ilen apply(simp)
          apply(rule index_less) 
            apply(simp) using ilen apply(simp)
            apply(simp)
          apply(simp only: a jo) using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
          using True by auto   
        have "?i' = Suc (index xs (xs ! i))" unfolding i' using fstF sndF a by simp 
        then show ?thesis using ass ass2 jo by auto
      qed
    next
      case 4
      assume ass: "i < index xs q - Suc n"
      then have ass2: "i < index xs q - n" by auto
      moreover have "(i < index xs q - n ⟶ ?i'' = index xs (xs ! i))" using indH by auto
      ultimately have a: "?i'' = index xs (xs ! i)" by auto
      from ass2 have "i < index xs q" by auto
      then have ilen: "i < length xs" using indq dual_order.strict_trans by blast


      have jo: "index xs (xs ! i) = i" apply(rule index_nth_id) using ilen by(auto)
      have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
        using indq apply (simp add: less_imp_diff_less)
        apply(simp)
        apply(rule nth_index) apply(simp) using ilen apply(simp)
        apply(rule index_less) 
          apply(simp) using ilen apply(simp)
          apply(simp)
        apply(simp only: a jo) using ass by auto 
      have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
        using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
        apply(simp)
        apply(rule nth_index) apply(simp) using ilen apply(simp)
        apply(rule index_less) 
          apply(simp) using ilen apply(simp)
          apply(simp)
        apply(simp only: a jo) using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
        using ass by auto  
      have "?i' = (index xs (xs ! i))" unfolding i' using fstF sndF a by simp
      then show ?case using jo ass by auto
    qed
  next
    case False

    then have smalla: "index xs q - Suc n = index xs q - n" by auto
    then have nomore: "swaps [index xs q - Suc n..<index xs q] xs
            =swaps [index xs q - n..<index xs q] xs" by auto
    show "(index xs q < i ∧ i < length xs ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
     index xs q < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < length xs) ∧
    (index xs q = i ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n) ∧
    (index xs q - Suc n ≤ i ∧ i < index xs q ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = Suc (index xs (xs ! i)) ∧
     index xs q - Suc n < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ≤ index xs q) ∧
    (i < index xs q - Suc n ⟶
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
     index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < index xs q - Suc n)" 
      unfolding nomore smalla by (rule indH)
  qed
next
  case 0
  then show ?case apply(simp)
  proof (safe, goal_cases)
    case 1
    have " index xs (xs ! i) = i" apply(rule index_nth_id) using 1 by auto
    with 1 show ?case by auto
  next
    case 2
    have "xs ! index xs q = q" using 2 by(auto)
    with 2 show ?case by auto
  next
    case 3
    have a: "index xs q < length xs" apply(rule index_less) using 3 by auto
    have "index xs (xs ! i) = i" apply(rule index_nth_id) apply(fact 3(2)) using 3(3) a by auto
    with 3 show ?case by auto
  qed   
qed

lemma mtf2_forward_effect1:
  "q ∈ set xs ⟹ distinct xs ⟹ index xs q < i ∧ i < length xs 
      ⟹ index (mtf2 n q xs) (xs ! i) = index xs (xs ! i) ∧ index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs" and    
  mtf2_forward_effect2: "q ∈ set xs ⟹ distinct xs ⟹ index xs q = i
      ⟹ index (mtf2 n q xs) (xs!i) = index xs q - n ∧ index xs q - n = index (mtf2 n q xs) (xs!i)" and    
  mtf2_forward_effect3: "q ∈ set xs ⟹ distinct xs ⟹ index xs q - n ≤ i ∧ i < index xs q
      ⟹ index (mtf2 n q xs) (xs!i) = Suc (index xs (xs!i)) ∧ index xs q - n < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) ≤ index xs q" and    
  mtf2_forward_effect4: "q ∈ set xs ⟹ distinct xs ⟹ i < index xs q - n 
      ⟹ index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index (mtf2 n q xs) (xs!i) < index xs q - n"
apply(safe) using mtf2_effect by metis+

lemma yes[simp]: "index xs x < length xs 
      ⟹ (xs!index xs x ) = x" apply(rule nth_index) by (simp add: index_less_size_conv)

lemma mtf2_forward_effect1':
  "q ∈ set xs ⟹ distinct xs ⟹ index xs q < index xs x ∧ index xs x < length xs 
      ⟹ index (mtf2 n q xs) x = index xs x ∧ index xs q < index (mtf2 n q xs) x ∧ index (mtf2 n q xs) x < length xs"     
 using mtf2_forward_effect1[where xs=xs and i="index xs x"] yes
 by(auto)

lemma
 mtf2_forward_effect2': "q ∈ set xs ⟹ distinct xs ⟹ index xs q = index xs x
      ⟹ index (mtf2 n q xs) (xs!index xs x) = index xs q - n ∧ index xs q - n = index (mtf2 n q xs) (xs!index xs x)"
 using mtf2_forward_effect2[where xs=xs and i="index xs x"] 
by fast

lemma
  mtf2_forward_effect3': "q ∈ set xs ⟹ distinct xs ⟹ index xs q - n ≤ index xs x ⟹ index xs x < index xs q
      ⟹ index (mtf2 n q xs) (xs!index xs x) = Suc (index xs (xs!index xs x)) ∧ index xs q - n < index (mtf2 n q xs) (xs!index xs x) ∧ index (mtf2 n q xs) (xs!index xs x) ≤ index xs q" 
 using mtf2_forward_effect3[where xs=xs and i="index xs x"] 
by fast

lemma    
  mtf2_forward_effect4': "q ∈ set xs ⟹ distinct xs ⟹ index xs x < index xs q - n 
      ⟹ index (mtf2 n q xs) (xs!index xs x) = index xs (xs!index xs x) ∧ index (mtf2 n q xs) (xs!index xs x) < index xs q - n"
 using mtf2_forward_effect4[where xs=xs and i="index xs x"] 
by fast


lemma splitit: " (index xs q < i ∧ i < length xs  ⟹ P)
     ⟹ (index xs q = i ⟹ P)
     ⟹ (index xs q - n ≤ i ∧ i < index xs q ⟹ P)
     ⟹ (i < index xs q - n ⟹ P)
   ⟹ (i < length xs ⟹ P)"
by force


lemma mtf2_forward_beforeq: "q ∈ set xs ⟹ distinct xs ⟹ i < index xs q 
        ⟹ index (mtf2 n q xs) (xs!i) ≤ index xs q"
apply (cases "i < index xs q - n")
  using mtf2_forward_effect4 apply force
  using mtf2_forward_effect3 using leI by metis


lemma x_stays_before_y_if_y_not_moved_to_front:
  assumes "q ∈ set xs" "distinct xs" "x ∈ set xs" "y ∈ set xs" "y ≠ q"
   and "x < y in xs"
  shows "x < y in (mtf2 n q xs)"
proof - 
  from assms(3) obtain i where i: "i = index xs x" and i2: "i < length xs" by auto
  from assms(4) obtain j where j: "j = index xs y" and j2: "j < length xs" by auto
  have "x < y in xs ⟹ x < y in (mtf2 n q xs)"
  apply(cases i xs rule: splitit[where q=q and n=n])
     apply(simp add: i  assms(1,2) mtf2_forward_effect1' before_in_def)
     apply(cases j xs rule: splitit[where q=q and n=n])
      apply (metis before_in_def assms(1-3) i j less_imp_diff_less mtf2_effect nth_index set_mtf2)
      apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect2' before_in_def)
      apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect2' before_in_def)
      apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect3' before_in_def)
      apply(rule j2)
     apply(cases j xs rule: splitit[where q=q and n=n])
      apply (smt before_in_def assms(1-3) i j le_less_trans mtf2_forward_effect1 mtf2_forward_effect3 nth_index set_mtf2)
      using assms(4,5) j apply simp
      apply (smt Suc_leI before_in_def assms(1-3) i j le_less_trans lessI mtf2_forward_effect3 nth_index set_mtf2)
      apply (simp add: before_in_def i j)     
      apply(rule j2)
     apply(cases j xs rule: splitit[where q=q and n=n])
      apply (smt before_in_def assms(1-3) i j le_less_trans mtf2_forward_effect1 mtf2_forward_effect4 nth_index set_mtf2)
      using assms(4-5) j apply simp
      apply (smt before_in_def assms(1-3) i j le_less_trans less_imp_le_nat mtf2_forward_effect3 mtf2_forward_effect4 nth_index set_mtf2)
      apply (metis before_in_def assms(1-3) i j mtf2_forward_effect4 nth_index set_mtf2)     
      apply(rule j2)
     apply(rule i2) done
   with assms(6) show ?thesis by auto
qed


corollary swapped_by_mtf2: "q ∈ set xs ⟹ distinct xs ⟹ x ∈ set xs ⟹  y ∈ set xs ⟹ 
      x < y in xs ⟹ y < x in (mtf2 n q xs) ⟹ y = q"
apply(rule ccontr) using x_stays_before_y_if_y_not_moved_to_front not_before_in by (metis before_in_setD1)

lemma x_stays_before_y_if_y_not_moved_to_front_2dir: "q ∈ set xs ⟹ distinct xs ⟹ x ∈ set xs ⟹  y ∈ set xs ⟹ y ≠ q ⟹ 
      x < y in xs = x < y in (mtf2 n q xs)"
oops

lemma mtf2_backwards_effect1:
  assumes "index xs q < length xs" "q ∈ set xs" "distinct xs" 
    "index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs"
    "i < length xs"
  shows  "index xs q <  i ∧ i  < length xs"
proof -
  from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
  with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
  from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
  with assms mtf2_forward_effect3 have 2: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis
  from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
  with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis

  from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q <  i ∧ i  < length xs" by metis
qed

lemma mtf2_backwards_effect2:
  assumes "index xs q < length xs" "q ∈ set xs" "distinct xs" "index (mtf2 n q xs) (xs ! i) = index xs q - n"
    "i < length xs" 
    shows "index xs q = i"
proof - 
  from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
  with assms mtf2_forward_effect1 have 1: "~ (index xs q < i ∧ i < length xs)" by metis
  from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
  with assms mtf2_forward_effect3 have 2: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis
  from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
  with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis

  from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q = i" by metis
qed

lemma mtf2_backwards_effect3:
  assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
    "index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q"
    "i < length xs"
  shows "index xs q - n ≤ i ∧ i < index xs q"
proof -
  from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
  with assms mtf2_forward_effect1 have 2: "~ (index xs q <  i ∧ i  < length xs)" by metis
  from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
  with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
  from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
  with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis

  from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q - n ≤ i ∧ i < index xs q" by metis
qed


lemma mtf2_backwards_effect4:
  assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
   "index (mtf2 n q xs) (xs ! i) < index xs q - n"
   "i < length xs" 
  shows "i < index xs q - n"
proof - 
  from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
  with assms mtf2_forward_effect1 have 2: "~ (index xs q <  i ∧ i  < length xs)" by metis
  from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
  with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
  from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
  with assms mtf2_forward_effect3 have 3: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis

  from fullchar[OF assms(1)] assms(5) 1 2 3 show "i < index xs q - n" by metis
qed

lemma mtf2_backwards_effect4':
 assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
  "index (mtf2 n q xs) x < index xs q - n"
  "x ∈ set xs"
 shows "(index xs x) < index xs q - n"
 using assms mtf2_backwards_effect4[where xs=xs and i="index xs x"] yes
by auto

lemma 
  assumes distA: "distinct A" and
          asm: "q ∈ set A"
  shows 
      mtf2_mono:  "q< x in A ⟹ q < x in (mtf2 n q A)" and
      mtf2_q_after: "index (mtf2 n q A) q =  index A q - n"
proof -

    have lele: "(q < x in A ⟶ q < x in swaps [index A q - n..<index A q] A) ∧ (index (swaps [index A q - n..<index A q] A) q =  index A q - n)"
    apply(induct n) apply(simp)
    proof -
      fix n
      assume ind: "(q < x in A ⟶ q < x in swaps [index A q - n..<index A q] A)
            ∧ index (swaps [index A q - n..<index A q] A) q =  index A q - n"
      then have iH: " q < x in A ⟹ q < x in swaps [index A q - n..<index A q] A" by auto
      from ind have indH2: "index (swaps [index A q - n..<index A q] A) q =  index A q - n" by auto

      show "(q < x in A ⟶ q < x in swaps [index A q - Suc n..<index A q] A) ∧
          index (swaps [index A q - Suc n..<index A q] A) q = index A q - Suc n" (is "?part1 ∧ ?part2")
      proof (cases "index A q ≥ Suc n")
          case True    
          then have onemore: "[index A q - Suc n..<index A q] = (index A q - Suc n) # [index A q - n..<index A q]"
                using Suc_diff_Suc upt_rec by auto

          from onemore have yeah: "swaps [index A q - Suc n..<index A q] A
              = swap (index A q - Suc n) (swaps  [index A q - n..<index A q] A)" by auto


            from indH2 have gr: "index (swaps [index A q - n..<index A q] A) q =  Suc(index A q - Suc n)" using Suc_diff_Suc True by auto
            have whereisq: "swaps [index A q - n..<index A q] A ! Suc (index A q - Suc n) = q" 
                unfolding gr[symmetric] apply(rule nth_index) using asm by auto

          have indSi: "index A q < length A" using asm index_less by auto
          have 3: "Suc (index A q - Suc n) < length (swaps [index A q - n..<index A q] A)" using True
            apply(auto simp: Suc_diff_Suc asm) using indSi by auto
          have 1: "q ≠ swaps [index A q - n..<index A q] A ! (index A q - Suc n)"
              proof
                assume as: "q = swaps [index A q - n..<index A q] A ! (index A q - Suc n)"
                {
                  fix xs x
                  have "Suc x < length xs ⟹ xs ! x = q ⟹ xs ! Suc x = q ⟹ ¬ distinct xs"  
                  by (metis Suc_lessD index_nth_id n_not_Suc_n)
                } note cool=this

                have "¬ distinct (swaps [index A q - n..<index A q] A)"
                  apply(rule cool[of "(index A q - Suc n)"])
                    apply(simp only: 3)
                    apply(simp only: as[symmetric])
                    by(simp only: whereisq)
                then show "False" using distA by auto 
              qed

          have part1: ?part1
          proof
            assume qx: "q < x in A"
            {  
              fix q x B i
               assume a1: "q < x in B"
               assume a2: "~ q = B ! i"
               assume a3: "distinct B"
               assume a4: "Suc i < length B"

               have "dist_perm B B" by(simp add: a3)
               moreover have "Suc i < length B" using a4 by auto
               moreover have "q < x in B ∧ ¬ (q = B ! i ∧ x = B ! Suc i)" using a1 a2 by auto
               ultimately have "q < x in swap i B"
                using before_in_swap[of B B] by simp
           } note grr=this

            have 2: "distinct (swaps [index A q - n..<index A q] A)" using distA by auto
            

            show "q < x in swaps [index A q - Suc n..<index A q] A"
              apply(simp only: yeah)
              apply(rule grr[OF iH[OF qx]]) using 1 2 3 by auto
           qed


           let ?xs = "(swaps [index A q - n..<index A q] A)"
           let ?n = "(index A q - Suc n)" 
           have "?xs ! Suc ?n = swaps [index A q - n..<index A q] A ! (index (swaps [index A q - n..<index A q] A) q)" 
              using indH2 Suc_diff_Suc True by auto
           also have "… = q" apply(rule nth_index) using asm by auto
           finally have sndTrue: "?xs ! Suc ?n = q" .
           have fstFalse: "~ q = ?xs ! ?n" by (fact 1) 


           have "index (swaps [index A q - Suc n..<index A q] A) q
              = index (swap (index A q - Suc n) ?xs) q" by (simp only: yeah) 
           also have "… = (if q = ?xs ! ?n then Suc ?n else if q = ?xs ! Suc ?n then ?n else index ?xs q)"
            apply(rule index_swap_distinct)
              apply(simp add: distA)
              by (fact 3)
           also have "… = ?n" using fstFalse sndTrue by auto
           finally have part2: ?part2 .

           from part1 part2 show "?part1 ∧ ?part2" by simp
        next 
          case False
          then have a: "index A q - Suc n = index A q - n" by auto
          then have b: "[index A q - Suc n..<index A q] = [index A q - n..<index A q]" by auto
          show ?thesis apply(simp only: b a) by (fact ind) 
        qed      
      qed 
 
    show "q < x in A ⟹ q < x in (mtf2 n q A)"
        "(index (mtf2 n q A) q) =  index A q - n"
    unfolding mtf2_def  
      using asm lele apply(simp)
      using asm lele by(simp)
qed




subsection "effect of mtf2 on index"

lemma swapsthrough: "distinct xs ⟹ q ∈ set xs ⟹ index ( swaps [index xs q - entf..<index xs q] xs ) q = index xs q - entf"
proof (induct entf)
  case (Suc e)
  note iH=this
  show ?case
  proof (cases "index xs q - e")
    case 0
    then have "[index xs q - Suc e..<index xs q]
        = [index xs q - e..<index xs q]" by force
    then have "index (swaps [index xs q - Suc e..<index xs q] xs) q
          =  index xs q - e" using Suc by auto
    also have "… = index xs q - (Suc e)" using 0 by auto
    finally show "index (swaps [index xs q - Suc e..<index xs q] xs) q = index xs q - Suc e" .
  next
    case (Suc f)

    have gaa: "Suc (index xs q - Suc e) = index xs q - e" using Suc by auto

    from Suc have "index xs q - e ≤ index xs q" by auto
    also have "… < length xs" by(simp add: index_less_size_conv iH)
    finally have indle: "index xs q - e < length xs".

    have arg: "Suc (index xs q - Suc e) < length (swaps [index xs q - e..<index xs q] xs)"
      apply(auto) unfolding gaa using indle by simp
    then have arg2: "index xs q - Suc e < length (swaps [index xs q - e..<index xs q] xs)" by auto
    from Suc have nexter: "index xs q - e = Suc (index xs q - (Suc e))" by auto
    then have aaa: "[index xs q - Suc e..<index xs q]
        = (index xs q - Suc e)#[index xs q - e..<index xs q]" using upt_rec by auto

     
    let ?i="index xs q - Suc e"
    let ?rest="swaps [index xs q - e..<index xs q] xs"
    from iH nexter have indj: "index ?rest q = Suc ?i" by auto

    from iH(2) have "distinct ?rest" by auto

    have "?rest ! (index ?rest q) = q" apply(rule nth_index) by(simp add: iH)
    with indj have whichcase: "q = ?rest ! Suc ?i" by auto

    with ‹distinct ?rest› have whichcase2: "~ q = ?rest ! ?i" 
          by (metis Suc_lessD arg index_nth_id n_not_Suc_n)

    from aaa have "index (swaps [index xs q - Suc e..<index xs q] xs) q
        = index (swap (index xs q - Suc e) (swaps [index xs q - e..<index xs q] xs)) q" 
          by auto
    also have "… = (if q = ?rest ! ?i then (Suc ?i) else if q = ?rest ! (Suc ?i) then ?i else index ?rest q)"
        apply(simp only: swap_def arg if_True)
        apply(rule index_swap_if_distinct)
          apply(simp add: iH)
          apply(simp only: arg2)
          by(simp only: arg)
    also have "… = ?i" using whichcase whichcase2 by simp
    finally show "index (swaps [index xs q - Suc e..<index xs q] xs) q =
              index xs q - Suc e" .
  qed
next
  case 0
  show ?case by simp
qed

term "mtf2"
lemma mtf2_moves_to_front: "distinct xs ⟹ q ∈ set xs ⟹ index (mtf2 (length xs) q xs) q  = 0"
unfolding mtf2_def
proof -
  assume distxs: "distinct xs"
  assume qinxs: "q ∈ set xs"
  have " index (if q ∈ set xs then swaps [index xs q - length xs..<index xs q] xs else xs) q 
    = index ( swaps [index xs q - length xs..<index xs q] xs) q" using qinxs by auto
  also have "… = index xs q - (length xs)" apply(rule swapsthrough) using distxs qinxs by auto
  also have "… = 0" using index_less_size_conv qinxs by (simp add: index_le_size)
  finally show "index (if q ∈ set xs then swaps [index xs q - length xs..<index xs q] xs else xs) q = 0" .
qed




lemma xy_relativorder_mtf2:
  assumes 
    "q≠x" "q≠y" "distinct xs" "x∈set xs" "y∈set xs" "q∈set xs"
  shows "x < y in mtf2 n q xs
          = x < y in xs"
using assms
by (metis before_in_setD2 not_before_in x_stays_before_y_if_y_not_moved_to_front)



lemma mtf2_moves_to_frontm1: "distinct xs ⟹ q ∈ set xs ⟹ index (mtf2 (length xs -1) q xs) q  = 0"
unfolding mtf2_def
proof -
  assume distxs: "distinct xs"
  assume qinxs: "q ∈ set xs"
  have " index (if q ∈ set xs then swaps [index xs q - (length xs -1)..<index xs q] xs else xs) q 
    = index ( swaps [index xs q - (length xs -1)..<index xs q] xs) q" using qinxs by auto
  also have "… = index xs q - (length xs -1)" apply(rule swapsthrough) using distxs qinxs by auto
  also have "… = 0" using index_less_size_conv qinxs 
by (metis Suc_pred' gr0I length_pos_if_in_set less_irrefl less_trans_Suc zero_less_diff)
  finally show "index (if q ∈ set xs then swaps [index xs q - (length xs -1)..<index xs q] xs else xs) q = 0" .
qed

lemma mtf2_moves_to_front': "distinct xs ⟹ y ∈ set xs ⟹ x ∈ set xs ⟹ x≠y ⟹ x < y in mtf2 (length xs-1) x xs = True"
using mtf2_moves_to_frontm1 by (metis before_in_def gr0I index_eq_index_conv set_mtf2)

lemma mtf2_moves_to_front'': "distinct xs ⟹ y ∈ set xs ⟹ x ∈ set xs ⟹ x≠y ⟹ x < y in mtf2 (length xs) x xs = True"
using mtf2_moves_to_front by (metis before_in_def gr0I index_eq_index_conv set_mtf2)




end