Theory OPT2

theory OPT2
imports Partial_Cost_Model RExp_Var
(*  Title:       Analysis of OPT2
    Author:      Max Haslbeck
*)

section "OPT2"

theory OPT2
imports 
Partial_Cost_Model
RExp_Var
begin

lemma "(N::nat set) ≠ {} ⟹ Inf N : N"
unfolding Inf_nat_def using LeastI[of "%x. x : N"] by force

lemma nn_contains_Inf:
  fixes S :: "nat set"
  assumes nn: "S ≠ {}"
  shows "Inf S ∈ S"
using assms Inf_nat_def LeastI by force


subsection "Definition"

fun OPT2 :: "'a list ⇒ 'a list ⇒ (nat * nat list) list" where
  "OPT2 [] [x,y] = []"
| "OPT2 [a] [x,y] = [(0,[])]"
| "OPT2 (a#b#σ') [x,y] =  (if a=x then (0,[]) # (OPT2 (b#σ') [x,y])
                                  else (if b=x then (0,[])# (OPT2 (b#σ') [x,y])
                                               else (1,[])# (OPT2 (b#σ') [y,x])))"
         

lemma OPT2_length: "length (OPT2 σ [x, y]) = length σ"
apply(induct σ arbitrary: x y)
  apply(simp)
  apply(case_tac σ) by(auto)

lemma OPT2x: "OPT2 (x#σ') [x,y] = (0,[])#(OPT2 σ' [x,y])"
apply(cases σ') by (simp_all)

 
lemma swapOpt: "Tp_opt [x,y] σ ≤ 1 + Tp_opt [y,x] σ"
proof -
  show ?thesis
  proof (cases "length σ > 0")
    case True

    have "Tp_opt [y,x] σ ∈ {Tp [y, x] σ as |as. length as = length σ}"
    unfolding T_opt_def 
      apply(rule nn_contains_Inf)
      apply(auto) by (rule Ex_list_of_length)

    then obtain asyx where costyx: "Tp [y,x] σ asyx = Tp_opt [y,x] σ"
                       and lenyx: "length asyx = length σ"
              unfolding T_opt_def by auto

    from True lenyx have "length asyx > 0" by auto
    then obtain A asyx' where aa: "asyx = A # asyx'" using list.exhaust by blast
    then obtain m1 a1 where AA: "A = (m1,a1)" by fastforce
    
    let ?asxy = "(m1,a1@[0]) # asyx'"
    
    from True obtain q σ' where qq: "σ = q # σ'" using list.exhaust by blast
  
    have t: "tp [x, y] q (m1, a1@[0]) = Suc (tp [y, x] q (m1, a1))"
    unfolding tp_def
    apply(simp) unfolding swap_def by (simp)
  
    have s: "step [x, y] q (m1, a1 @ [0]) = step [y, x] q (m1, a1)" 
    unfolding step_def mtf2_def by(simp add: swap_def)
  
    have T: "Tp [x,y] σ ?asxy = 1 + Tp [y,x] σ asyx" unfolding qq aa AA by(auto simp add: s t)
   
    have l: "1 + Tp_opt [y,x] σ = Tp [x, y] σ ?asxy" using T costyx by simp
    have "length ?asxy = length σ" using lenyx aa by auto
    then have inside: "?asxy ∈ {as. size as = size σ}" by force
    then have b: "Tp [x, y] σ ?asxy ∈ {Tp [x, y] σ as | as. size as = size σ}" by auto

    then show ?thesis unfolding l unfolding T_opt_def
      apply(rule cInf_lower) by simp
  qed (simp add: T_opt_def)         
qed


lemma tt: "a ∈ {x,y} ⟹ OPT2 (rest1) (step [x,y] a (hd (OPT2 (a # rest1) [x, y])))
       = tl (OPT2 (a # rest1) [x, y])"
apply(cases rest1) by(auto simp add: step_def mtf2_def swap_def)

lemma splitqsallg: "Strat ≠ [] ⟹ a ∈ {x,y} ⟹
         tp [x, y] a (hd (Strat)) +
          (let L=step [x,y] a (hd (Strat)) 
              in Tp L (rest1) (tl Strat)) =  Tp [x, y] (a # rest1) Strat"
proof -
  assume ne: "Strat ≠ []"
  assume axy: "a ∈ {x,y}" (* not needed *)
  have "Tp [x, y] (a # rest1) (Strat) 
        = Tp [x, y] (a # rest1) ((hd (Strat)) # (tl (Strat)))"
        by(simp only: List.list.collapse[OF ne])
  then show ?thesis by auto
qed

lemma splitqs: "a ∈ {x,y} ⟹ Tp [x, y] (a # rest1) (OPT2 (a # rest1) [x, y])
        =  tp [x, y] a (hd (OPT2 (a # rest1) [x, y])) +
          (let L=step [x,y] a (hd (OPT2 (a # rest1) [x, y])) 
              in Tp L (rest1) (OPT2 (rest1) L))"
proof -
  assume axy: "a ∈ {x,y}"
  have ne: "OPT2 (a # rest1) [x, y] ≠ []" apply(cases rest1) by(simp_all)
  have "Tp [x, y] (a # rest1) (OPT2 (a # rest1) [x, y]) 
        = Tp [x, y] (a # rest1) ((hd (OPT2 (a # rest1) [x, y])) # (tl (OPT2 (a # rest1) [x, y])))"
        by(simp only: List.list.collapse[OF ne])
  also have "… = Tp [x, y] (a # rest1) ((hd (OPT2 (a # rest1) [x, y])) # (OPT2 (rest1) (step [x,y] a (hd (OPT2 (a # rest1) [x, y])))))"
      by(simp only: tt[OF axy])
  also have "… =   tp [x, y] a (hd (OPT2 (a # rest1) [x, y])) +
          (let L=step [x,y] a (hd (OPT2 (a # rest1) [x, y])) 
              in Tp L (rest1) (OPT2 (rest1) L))" by(simp)
  finally show ?thesis .
qed

lemma tpx: "tp [x, y] x (hd (OPT2 (x # rest1) [x, y])) = 0"
by (simp add: OPT2x tp_def)

lemma yup: "Tp [x, y] (x # rest1) (OPT2 (x # rest1) [x, y])
        = (let L=step [x,y] x (hd (OPT2 (x # rest1) [x, y])) 
              in Tp L (rest1) (OPT2 (rest1) L))"
by (simp add: splitqs tpx)

lemma swapsxy: "A ∈ { [x,y], [y,x]} ⟹ swaps sws A ∈ { [x,y], [y,x]}"
apply(induct sws)
  apply(simp)
  apply(simp) unfolding swap_def by auto

lemma mtf2xy: "A ∈ { [x,y], [y,x]} ⟹ r∈{x,y} ⟹ mtf2 a r A ∈ { [x,y], [y,x]}"
by (metis mtf2_def swapsxy)


lemma stepxy: assumes "q ∈ {x,y}" "A ∈ { [x,y], [y,x]}" 
    shows "step A q a ∈ { [x,y], [y,x]}"
unfolding step_def apply(simp only: split_def Let_def)
apply(rule mtf2xy)
  apply(rule swapsxy) by fact+ 


subsection "Proof of Optimality"

lemma OPT2_is_lb: "set σ ⊆ {x,y} ⟹ x≠y ⟹ Tp [x,y] σ (OPT2 σ [x,y]) ≤ Tp_opt [x,y] σ" 
proof (induct "length σ" arbitrary: x y σ rule: less_induct)
  case (less)
  show ?case
  proof (cases σ)
    case (Cons a σ')
    note Cons1=Cons
    show ?thesis unfolding Cons
      proof(cases "a=x") (* case that the element in front is requested *)
        case True
        from True Cons have qsform: "σ = x#σ'" by auto
        have up: "Tp [x, y] (x # σ') (OPT2 (x # σ') [x, y]) ≤ Tp_opt [x, y] (x # σ')"
          unfolding True
          unfolding T_opt_def apply(rule cInf_greatest)
            apply(simp add: Ex_list_of_length)
            proof -
              fix el
              assume "el ∈ {Tp [x, y] (x # σ') as |as. length as = length (x # σ')}"
              then obtain Strat where lStrat: "length Strat = length (x # σ')"
                        and el: "Tp [x, y] (x # σ') Strat = el" by auto
              then have ne: "Strat ≠ []" by auto
              let ?LA="step [x,y] x (hd (OPT2 (x # σ') [x, y]))"
              
              have  E0:  "Tp [x, y] (x # σ') (OPT2 (x # σ') [x, y])
                            =Tp ?LA (σ') (OPT2 (σ') ?LA)" using yup by auto
              also have E1: "… = Tp [x,y] (σ') (OPT2 (σ') [x,y])" by (simp add: OPT2x step_def)
              also have E2: "… ≤  Tp_opt [x,y] σ'" apply(rule less(1)) using Cons less(2,3) by auto
              also have "… ≤ Tp [x, y] (x # σ') Strat"
                   proof (cases "(step [x, y] x (hd Strat)) = [x,y]")
                      case True
                      have aha: "Tp_opt [x, y] σ' ≤ Tp [x, y] σ' (tl Strat)"                     
                        unfolding T_opt_def apply(rule cInf_lower)
                          apply(auto) apply(rule exI[where x="tl Strat"]) using lStrat by auto

                      also have E4: "… ≤ tp [x, y] x (hd Strat) + Tp (step [x, y] x (hd Strat)) σ' (tl Strat)" 
                        unfolding True by(simp)
                      also have E5: "… = Tp [x, y] (x # σ') Strat" using splitqsallg[of Strat x x y σ', OF ne, simplified]
                        by (auto)
                      finally show ?thesis by auto 
                   next
                      case False
                      have tp1: "tp [x, y] x (hd Strat) ≥ 1"
                      proof (rule ccontr)
                        let ?a = "hd Strat"
                        assume "¬ 1 ≤ tp [x, y] x ?a"
                        then have tp0: "tp [x, y] x ?a = 0" by auto
                        then have "size (snd ?a) = 0" unfolding tp_def by(simp add: split_def)
                        then have nopaid: "(snd ?a) = []" by auto
                        have "step [x, y] x ?a = [x, y]"
                          unfolding step_def apply(simp add: split_def nopaid)
                          unfolding mtf2_def by(simp)
                        then show "False" using False by auto
                      qed

                      from False have yx: "step [x, y] x (hd Strat) = [y, x]"
                        using stepxy[where x=x and y=y and a="hd Strat"] by auto

                      have E3: "Tp_opt [x, y] σ' ≤ 1 + Tp_opt [y, x] σ'" using swapOpt by auto
                      also have E4: "… ≤ 1 + Tp [y, x] σ' (tl Strat)"        
                        apply(simp) unfolding T_opt_def apply(rule cInf_lower)
                          apply(auto) apply(rule exI[where x="tl Strat"]) using lStrat by auto
                      also have E5: "… = 1 + Tp (step [x, y] x (hd Strat)) σ' (tl Strat)" using yx by auto
                      also have E6: "… ≤ tp [x, y] x (hd Strat) + Tp (step [x, y] x (hd Strat)) σ' (tl Strat)" using tp1 by auto
                      
                      also have E7: "… = Tp [x, y] (x # σ') Strat" using splitqsallg[of Strat x x y σ', OF ne, simplified]
                         by (auto)
                      finally show ?thesis by auto
                   qed
              also have "… = el" using True el by simp
              finally show "Tp [x, y] (x # σ') (OPT2 (x # σ') [x, y]) ≤ el" by auto        
            qed
         then show "Tp [x, y] (a # σ') (OPT2 (a # σ') [x, y]) ≤ Tp_opt [x, y] (a # σ')"
         using True by simp
      next


        case False (* case 2: element at back is requested first *)
        with less Cons have ay: "a=y" by auto
        show "Tp [x, y] (a # σ') (OPT2 (a # σ') [x, y]) ≤ Tp_opt [x, y] (a # σ')" unfolding ay
        proof(cases σ')
          case Nil
          have up: "Tp_opt [x, y] [y] ≥ 1"
            unfolding T_opt_def apply(rule cInf_greatest)
            apply(simp add: Ex_list_of_length)
            proof -
              fix el
              assume "el ∈ {Tp [x, y] [y] as |as. length as = length [y]}"
              then obtain Strat where Strat: "length Strat = length [y]" and
                            el: "el = Tp [x, y] [y] Strat " by auto
              from Strat obtain a where a: "Strat = [a]" by (metis Suc_length_conv length_0_conv)
              show "1 ≤ el" unfolding el a apply(simp) unfolding tp_def apply(simp add: split_def)
                apply(cases "snd a")
                  apply(simp add: less(3))
                  by(simp)
            qed

          show "Tp [x, y] (y # σ') (OPT2 (y # σ') [x, y]) ≤ Tp_opt [x, y] (y # σ')" unfolding Nil
            apply(simp add: tp_def) using less(3) apply(simp)
            using up by(simp)
        next
          case (Cons b rest2)

          show up: "Tp [x, y] (y # σ') (OPT2 (y # σ') [x, y]) ≤ Tp_opt [x, y] (y # σ')"
            unfolding Cons
          proof (cases "b=x")
            case True
            
            show "Tp [x, y] (y # b # rest2) (OPT2 (y # b # rest2) [x, y]) ≤ Tp_opt [x, y] (y # b # rest2)"
              unfolding True
              unfolding T_opt_def apply(rule cInf_greatest)
                apply(simp add: Ex_list_of_length)
                proof -
                  fix el
                  assume "el ∈ {Tp [x, y] (y # x # rest2) as |as. length as = length (y # x # rest2)}"
                  then obtain Strat where lenStrat: "length Strat = length (y # x # rest2)" and
                               Strat: "el = Tp [x, y] (y # x # rest2) Strat" by auto
                  have v: " set rest2 ⊆ {x, y}" using less(2)[unfolded Cons1 Cons] by auto
                  
                  let ?L1 = "(step [x, y] y (hd Strat))"
                  let ?L2 = "(step ?L1 x (hd (tl Strat)))"

                  (* lets work on how Strat can look like: *)
                  let ?a1 = "hd Strat"
                  let ?a2 = "hd (tl Strat)"
                  let ?r = "tl (tl Strat)"

                  have "Strat = ?a1 # ?a2 # ?r" by (metis Nitpick.size_list_simp(2) Suc_length_conv lenStrat list.collapse list.discI list.inject)
                  
                  


                  have 1: "Tp [x, y] (y # x # rest2) Strat
                        = tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat))
                            + Tp ?L2 rest2 (tl (tl Strat))"  
                    proof - 
                      have a: "Strat ≠ []" using lenStrat by auto
                      have b: "(tl Strat) ≠ []" using lenStrat by (metis Nitpick.size_list_simp(2) Suc_length_conv list.discI list.inject)

                      have 1: "Tp [x, y] (y # x # rest2) Strat
                                = tp [x, y] y (hd Strat) + Tp ?L1 (x # rest2) (tl Strat)"
                                  using splitqsallg[OF a, where a=y and x=x and y=y, simplified] by (simp)
                      have tt: "step [x, y] y (hd Strat) ≠ [x, y] ⟹ step [x, y] y (hd Strat) = [y,x]" 
                        using stepxy[where A="[x,y]"] by blast

                      have 2: "Tp ?L1 (x # rest2) (tl Strat) = tp ?L1 x (hd (tl Strat)) +  Tp ?L2 (rest2) (tl (tl Strat))"
                                  apply(cases "?L1=[x,y]")
                                    using splitqsallg[OF b, where a=x and x=x and y=y, simplified] apply(auto)
                                    using tt splitqsallg[OF b, where a=x and x=y and y=x, simplified] by auto
                      from 1 2 show ?thesis by auto
                    qed

                  have " Tp [x, y] (y # x # rest2) (OPT2 (y # x # rest2) [x, y])
                    =  1 +  Tp [x, y] (rest2) (OPT2 (rest2) [x, y])"
                    unfolding True
                    using less(3) by(simp add: tp_def step_def OPT2x)
                  also have "… ≤ 1 +  Tp_opt [x, y] (rest2)" apply(simp)
                    apply(rule less(1))
                      apply(simp add: less(2) Cons1 Cons)
                      apply(fact) by fact
                  also

                  have "… ≤ Tp [x, y] (y # x # rest2) Strat"
                  proof (cases "?L2 = [x,y]")
                    case True
                    have 2: "tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat))
                            + Tp [x,y] rest2 (tl (tl Strat)) ≥ tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat))
                            + Tp_opt [x,y] rest2" apply(simp)
                            unfolding T_opt_def apply(rule cInf_lower)
                            apply(simp) apply(rule exI[where x="tl (tl Strat)"]) by (auto simp: lenStrat)
                    have 3: "tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat))
                            + Tp_opt [x,y] rest2 ≥ 1 + Tp_opt [x,y] rest2" apply(simp)
                            proof -
                              have "tp [x, y] y (hd Strat) ≥ 1"
                              unfolding tp_def apply(simp add: split_def)
                              apply(cases "snd (hd Strat)") by (simp_all add: less(3))
                              then show "Suc 0 ≤ tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat))" by auto
                            qed
                    from 1 2 3 True show ?thesis by auto
                  next
                    case False
                    note L2F=this
                    have L1: "?L1 ∈ {[x, y], [y, x]}" apply(rule stepxy) by simp_all
                    have "?L2 ∈ {[x, y], [y, x]}" apply(rule stepxy) using L1 by simp_all
                    with False have 2: "?L2 = [y,x]" by auto

                    have k: "Tp [x, y] (y # x # rest2) Strat
                        =   tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat)) +
                            Tp [y,x] rest2 (tl (tl Strat))" using 1 2 by auto

                    have l: "tp [x, y] y (hd Strat) > 0"
                        using less(3) unfolding tp_def apply(cases "snd (hd Strat) = []")
                          by (simp_all add: split_def)

                    have r: "Tp [x, y] (y # x # rest2) Strat ≥ 2 + Tp [y,x] rest2 (tl (tl Strat))"
                    proof (cases "?L1 = [x,y]")
                      case True
                      note T=this
                      then have "tp ?L1 x (hd (tl Strat)) > 0" unfolding True
                        proof(cases "snd (hd (tl Strat)) = []")
                          case True
                          have "?L2 = [x,y]" unfolding T  apply(simp add: split_def step_def) 
                          unfolding True mtf2_def by(simp)
                          with L2F have "False" by auto
                          then show "0 < tp [x, y] x (hd (tl Strat))" ..
                        next
                          case False
                          then show "0 < tp [x, y] x (hd (tl Strat))"
                            unfolding tp_def by(simp add: split_def)
                        qed                          
                      with l have " tp [x, y] y (hd Strat) + tp ?L1 x (hd (tl Strat)) ≥ 2" by auto
                      with k show ?thesis by auto
                    next
                      case False
                      from L1 False have 2: "?L1 = [y,x]" by auto
                      { fix k sws T
                        have "T∈{[x,y],[y,x]} ⟹ mtf2 k x T = [y,x] ⟹ T = [y,x]"
                          apply(rule ccontr) by (simp add: less(3) mtf2_def)
                      }
                      have t1: "tp [x, y] y (hd Strat) ≥ 1" unfolding tp_def apply(simp add: split_def)
                        apply(cases "(snd (hd Strat))") using ‹x ≠ y› by auto
                      have t2: "tp [y,x] x (hd (tl Strat)) ≥ 1" unfolding tp_def apply(simp add: split_def)
                        apply(cases "(snd (hd (tl Strat)))") using ‹x ≠ y› by auto
                      have "Tp [x, y] (y # x # rest2) Strat
                          = tp [x, y] y (hd Strat) + tp (step [x, y] y (hd Strat)) x (hd (tl Strat)) + Tp [y, x] rest2 (tl (tl Strat))"
                            by(rule k)
                      with t1 t2 2 show ?thesis by auto
                    qed
                    have t: "Tp [y, x] rest2 (tl (tl Strat)) ≥ Tp_opt [y, x] rest2" 
                      unfolding T_opt_def apply(rule cInf_lower)
                      apply(auto) apply(rule exI[where x="(tl (tl Strat))"]) by(simp add: lenStrat)
                    show ?thesis
                    proof -
                      have "1 + Tp_opt [x, y] rest2 ≤ 2 + Tp_opt [y, x] rest2"
                      using  swapOpt by auto
                      also have "… ≤ 2 + Tp [y, x] rest2 (tl (tl Strat))" using t by auto
                      also have "… ≤ Tp [x, y] (y # x # rest2) Strat" using r by auto
                      finally show ?thesis .
                    qed
                      
                  qed
                  also have "… = el" using Strat by auto
                  finally show "Tp [x, y] (y # x # rest2) (OPT2 (y # x # rest2) [x, y]) ≤ el" .
                qed


          next
            case False
            with Cons1 Cons less(2) have bisy: "b=y" by auto
            with less(3) have "OPT2 (y # b # rest2) [x, y] = (1,[])# (OPT2 (b#rest2) [y,x])" by simp
            show "Tp [x, y] (y # b # rest2) (OPT2 (y # b # rest2) [x, y]) ≤ Tp_opt [x, y] (y # b # rest2)" 
              unfolding bisy
              unfolding T_opt_def apply(rule cInf_greatest)
                apply(simp add: Ex_list_of_length)
                proof -
                  fix el
                  assume "el ∈ {Tp [x, y] (y # y # rest2) as |as. length as = length (y # y # rest2)}"
                  then obtain Strat where lenStrat: "length Strat = length (y # y # rest2)" and
                               Strat: "el = Tp [x, y] (y # y # rest2) Strat" by auto
                  have v: " set rest2 ⊆ {x, y}" using less(2)[unfolded Cons1 Cons] by auto

                  let ?L1 = "(step [x, y] y (hd Strat))"
                  let ?L2 = "(step ?L1 y (hd (tl Strat)))"

                  (* lets work on how Strat can look like: *)
                  let ?a1 = "hd Strat"
                  let ?a2 = "hd (tl Strat)"
                  let ?r = "tl (tl Strat)"

                  have "Strat = ?a1 # ?a2 # ?r" by (metis Nitpick.size_list_simp(2) Suc_length_conv lenStrat list.collapse list.discI list.inject)
                  
                  


                  have 1: "Tp [x, y] (y # y # rest2) Strat
                        = tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat))
                            + Tp ?L2 rest2 (tl (tl Strat))" 
                    proof - 
                      have a: "Strat ≠ []" using lenStrat by auto
                      have b: "(tl Strat) ≠ []" using lenStrat by (metis Nitpick.size_list_simp(2) Suc_length_conv list.discI list.inject)

                      have 1: "Tp [x, y] (y # y # rest2) Strat
                                = tp [x, y] y (hd Strat) + Tp ?L1 (y # rest2) (tl Strat)"
                                  using splitqsallg[OF a, where a=y and x=x and y=y, simplified] by (simp)
                      have tt: "step [x, y] y (hd Strat) ≠ [x, y] ⟹ step [x, y] y (hd Strat) = [y,x]" 
                        using stepxy[where A="[x,y]"] by blast
                     
                      have 2: "Tp ?L1 (y # rest2) (tl Strat) = tp ?L1 y (hd (tl Strat)) +  Tp ?L2 (rest2) (tl (tl Strat))"
                                  apply(cases "?L1=[x,y]")
                                    using splitqsallg[OF b, where a=y and x=x and y=y, simplified] apply(auto)
                                    using tt splitqsallg[OF b, where a=y and x=y and y=x, simplified] by auto
                      from 1 2 show ?thesis by auto
                    qed

                  have " Tp [x, y] (y # y # rest2) (OPT2 (y # y # rest2) [x, y])
                    =  1 +  Tp [y, x] (rest2) (OPT2 (rest2) [y, x])" 
                    using less(3) by(simp add: tp_def step_def mtf2_def swap_def OPT2x)
                  also have "… ≤ 1 +  Tp_opt [y, x] (rest2)" apply(simp)
                    apply(rule less(1))
                      apply(simp add: less(2) Cons1 Cons)
                      using v less(3) by(auto)
                  also

                  have "… ≤ Tp [x, y] (y # y # rest2) Strat"
                  proof (cases "?L2 = [y,x]")
                    case True
                    have 2: "tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat))
                            + Tp [y,x] rest2 (tl (tl Strat)) ≥ tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat))
                            + Tp_opt [y,x] rest2" apply(simp)
                            unfolding T_opt_def apply(rule cInf_lower)
                            apply(simp) apply(rule exI[where x="tl (tl Strat)"]) by (auto simp: lenStrat)
                    have 3: "tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat))
                            + Tp_opt [y,x] rest2 ≥ 1 + Tp_opt [y,x] rest2" apply(simp)
                            proof -
                              have "tp [x, y] y (hd Strat) ≥ 1"
                              unfolding tp_def apply(simp add: split_def)
                              apply(cases "snd (hd Strat)") by (simp_all add: less(3))
                              then show "Suc 0 ≤ tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat))" by auto
                            qed
                    from 1 2 3 True show ?thesis by auto 
                  next
                    case False 
                    note L2F=this
                    have L1: "?L1 ∈ {[x, y], [y, x]}" apply(rule stepxy) by simp_all
                    have "?L2 ∈ {[x, y], [y, x]}" apply(rule stepxy) using L1 by simp_all
                    with False have 2: "?L2 = [x,y]" by auto

                    have k: "Tp [x, y] (y # y # rest2) Strat
                        =   tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat)) +
                            Tp [x,y] rest2 (tl (tl Strat))" using 1 2 by auto

                    have l: "tp [x, y] y (hd Strat) > 0"
                        using less(3) unfolding tp_def apply(cases "snd (hd Strat) = []")
                          by (simp_all add: split_def)

                    have r: "Tp [x, y] (y # y # rest2) Strat ≥ 2 + Tp [x,y] rest2 (tl (tl Strat))"
                    proof (cases "?L1 = [y,x]")  
                      case False
                      from L1 False have "?L1 = [x,y]" by auto
                      note T=this
                      then have "tp ?L1 y (hd (tl Strat)) > 0" unfolding T
                      unfolding tp_def apply(simp add: split_def)
                        apply(cases "snd (hd (tl Strat)) = []")
                          using ‹x ≠ y› by auto
                      with l k show ?thesis by auto
                    next

                      case True
                      note T=this
                          
                        have "tp ?L1 y (hd (tl Strat)) > 0" unfolding T
                        proof(cases "snd (hd (tl Strat)) = []")
                          case True
                          have "?L2 = [y,x]" unfolding T  apply(simp add: split_def step_def) 
                          unfolding True mtf2_def by(simp)
                          with L2F have "False" by auto
                          then show "0 < tp [y, x] y (hd (tl Strat))" ..
                        next
                          case False
                          then show "0 < tp [y, x] y (hd (tl Strat))"
                            unfolding tp_def by(simp add: split_def)
                        qed                          
                      with l have " tp [x, y] y (hd Strat) + tp ?L1 y (hd (tl Strat)) ≥ 2" by auto
                      with k show ?thesis by auto
                    
                    qed
                    have t: "Tp [x, y] rest2 (tl (tl Strat)) ≥ Tp_opt [x, y] rest2" 
                      unfolding T_opt_def apply(rule cInf_lower)
                      apply(auto) apply(rule exI[where x="(tl (tl Strat))"]) by(simp add: lenStrat)
                    show ?thesis
                    proof -
                      have "1 + Tp_opt [y, x] rest2 ≤ 2 + Tp_opt [x, y] rest2"
                      using  swapOpt by auto
                      also have "… ≤ 2 + Tp [x, y] rest2 (tl (tl Strat))" using t by auto
                      also have "… ≤ Tp [x, y] (y # y # rest2) Strat" using r by auto
                      finally show ?thesis .
                    qed
                      
                  qed
                  also have "… = el" using Strat by auto
                  finally show "Tp [x, y] (y # y # rest2) (OPT2 (y # y # rest2) [x, y]) ≤ el" .
                qed
          qed
        qed
     qed
  qed (simp add: T_opt_def)
qed


lemma OPT2_is_ub: "set qs ⊆ {x,y} ⟹ x≠y ⟹ Tp [x,y] qs (OPT2 qs [x,y]) ≥ Tp_opt [x,y] qs"
  unfolding T_opt_def apply(rule cInf_lower)
            apply(simp) apply(rule exI[where x="(OPT2 qs [x, y])"])
            by (auto simp add: OPT2_length)



lemma OPT2_is_opt: "set qs ⊆ {x,y} ⟹ x≠y ⟹ Tp [x,y] qs (OPT2 qs [x,y]) = Tp_opt [x,y] qs"
by (simp add: OPT2_is_lb OPT2_is_ub antisym)


subsection "Performance on the four phase forms"

lemma OPT2_A: assumes "x ≠ y" "qs ∈ lang (seq [Plus (Atom x) One, Atom y, Atom y])"
  shows "Tp [x,y] qs (OPT2 qs [x,y]) = 1"
proof -
  from assms(2) obtain u v where qs: "qs=u@v" and u: "u=[x] ∨ u=[]" and v: "v = [y,y]" by (auto simp: conc_def)
  from u have pref1: "Tp [x,y] (u@v) (OPT2 (u@v) [x,y]) = Tp [x,y] v (OPT2 v [x,y])"
    apply(cases "u=[]")
      apply(simp)
      by(simp add: OPT2x tp_def step_def)

  have ende: "Tp [x,y] v (OPT2 v [x,y]) = 1" unfolding v using assms(1) by(simp add: mtf2_def swap_def tp_def step_def)

  from pref1 ende qs show ?thesis by auto
qed
  

lemma OPT2_A': assumes "x ≠ y" "qs ∈ lang (seq [Plus (Atom x) One, Atom y, Atom y])"
  shows "real (Tp [x,y] qs (OPT2 qs [x,y])) = 1"
using OPT2_A[OF assms] by simp


lemma OPT2_B: assumes "x ≠ y" "qs=u@v" "u=[] ∨ u=[x]" "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
  shows "Tp [x,y] qs (OPT2 qs [x,y]) = (length v div 2)"
proof -
  from assms(3) have pref1: "Tp [x,y] (u@v) (OPT2 (u@v) [x,y]) = Tp [x,y] v (OPT2 v [x,y])"
    apply(cases "u=[]")
      apply(simp)
      by(simp add: OPT2x tp_def step_def)

  from assms(4) obtain a w where v: "v=a@w" and "a∈lang (Times (Atom y) (Atom x))" and w: "w∈lang (seq[Star(Times (Atom y) (Atom x)), Atom y, Atom y])" by(auto)
  from this(2) have aa: "a=[y,x]" by(simp add: conc_def)

  from assms(1) this v have pref2: "Tp [x,y] v (OPT2 v [x,y]) = 1 + Tp [x,y] w (OPT2 w [x,y])"
   by(simp add: tp_def step_def OPT2x)

  from w obtain c d where w2: "w=c@d" and c: "c ∈ lang (Star (Times (Atom y) (Atom x)))" and d: "d ∈ lang (Times (Atom y) (Atom y))" by auto
  then have dd: "d=[y,y]" by auto

  from c[simplified] have star: "Tp [x,y] (c@d) (OPT2 (c@d) [x,y]) = (length c div 2) +  Tp [x,y] d (OPT2 d [x,y])"
    proof(induct c rule: star_induct)
      case (append r s)       
      then have r: "r=[y,x]" by auto
      then have "Tp [x, y] ((r @ s) @ d) (OPT2 ((r @ s) @ d) [x, y]) = Tp [x, y] ([y,x] @ (s @ d)) (OPT2 ([y,x] @ (s @ d)) [x, y])" by simp
      also have "… = 1 + Tp [x, y] (s @ d) (OPT2 (s @ d) [x, y])"
        using assms(1) by(simp add: tp_def step_def OPT2x)
      also have "… =  1 + length s div 2 + Tp [x, y] d (OPT2 d [x, y])" using append by simp
      also have "… =  length (r @ s) div 2 + Tp [x, y] d (OPT2 d [x, y])" using r by auto
      finally show ?case .
    qed simp

  have ende: "Tp [x,y] d (OPT2 d [x,y]) = 1" unfolding dd using assms(1) by(simp add: mtf2_def swap_def tp_def step_def)
  
  have vv: "v = [y,x]@c@[y,y]" using w2 dd v aa by auto

  from pref1 pref2 star w2 ende have
    "Tp [x, y] qs (OPT2 qs [x, y]) = 1 + length c div 2 + 1" unfolding assms(2) by auto
  also have "… = (length v div 2)" using vv by auto
  finally show ?thesis .
qed

lemma OPT2_B1: assumes "x ≠ y" "qs ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
  shows "real (Tp [x,y] qs (OPT2 qs [x,y])) = length qs / 2"
proof -
  from assms(2) have qs: "qs ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
    by(simp add: conc_assoc)
  have "(length qs) mod 2 = 0"
  proof -
    from assms(2) have "qs ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by (simp add: conc_assoc)
    then obtain p q r where pqr: "qs=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[y]} @@ {[y]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[y,y]" by auto
    with pqr have a: "length qs = 4+length q" by auto
    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b show ?thesis by auto
  qed
  with OPT2_B[where u="[]", OF assms(1) _ _ qs] show ?thesis by auto
qed  
  
lemma OPT2_B2: assumes "x ≠ y" "qs ∈ lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom y, Atom y])"
  shows "Tp [x,y] qs (OPT2 qs [x,y]) = ((length qs - 1) / 2)"
proof -
  from assms(2) obtain v where
      qsv: "qs = [x]@v" and vv: "v ∈ lang (seq[Times (Atom y) (Atom x), Star(Times (Atom y) (Atom x)), Atom y, Atom y])" by (auto simp add: conc_def)
  have "(length v) mod 2 = 0"
  proof -
    from vv have "v ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[y]} @@ {[y]}" by (simp add: conc_assoc)
    then obtain p q r where pqr: "v=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[y]} @@ {[y]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[y,y]" by(auto simp add: conc_def)
    with pqr have a: "length v = 4+length q" by auto
    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b show ?thesis by auto
  qed
  with OPT2_B[where u="[x]", OF assms(1) qsv _ vv] qsv show ?thesis by(auto)
qed 

lemma OPT2_C: assumes "x ≠ y" "qs=u@v" "u=[] ∨ u=[x]" 
  and "v ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
  shows "Tp [x,y] qs (OPT2 qs [x,y]) = (length v div 2)"
proof -
  from assms(3) have pref1: "Tp [x,y] (u@v) (OPT2 (u@v) [x,y]) = Tp [x,y] v (OPT2 v [x,y])"
    apply(cases "u=[]")
      apply(simp)
      by(simp add: OPT2x tp_def step_def)

  from assms(4) obtain a w where v: "v=a@w" and aa: "a=[y,x]" and w: "w∈lang (seq[Star(Times (Atom y) (Atom x)), Atom x])" by(auto simp: conc_def)

  from assms(1) this v have pref2: "Tp [x,y] v (OPT2 v [x,y]) = 1 + Tp [x,y] w (OPT2 w [x,y])"
   by(simp add: tp_def step_def OPT2x)

  from w obtain c d where w2: "w=c@d" and c: "c ∈ lang (Star (Times (Atom y) (Atom x)))" and d: "d ∈ lang (Atom x)" by auto
  then have dd: "d=[x]" by auto

  from c[simplified] have star: "Tp [x,y] (c@d) (OPT2 (c@d) [x,y]) = (length c div 2) +  Tp [x,y] d (OPT2 d [x,y]) ∧ (length c) mod 2 = 0"
    proof(induct c rule: star_induct)
      case (append r s)
      from append have mod: "length s mod 2 = 0" by simp
      from append have r: "r=[y,x]" by auto
      then have "Tp [x, y] ((r @ s) @ d) (OPT2 ((r @ s) @ d) [x, y]) = Tp [x, y] ([y,x] @ (s @ d)) (OPT2 ([y,x] @ (s @ d)) [x, y])" by simp
      also have "… = 1 + Tp [x, y] (s @ d) (OPT2 (s @ d) [x, y])"
        using assms(1) by(simp add: tp_def step_def OPT2x)
      also have "… =  1 + length s div 2 + Tp [x, y] d (OPT2 d [x, y])" using append by simp
      also have "… =  length (r @ s) div 2 + Tp [x, y] d (OPT2 d [x, y])" using r by auto
      finally show ?case by(simp add: mod r)
    qed simp

  have ende: "Tp [x,y] d (OPT2 d [x,y]) = 0" unfolding dd using assms(1) by(simp add: mtf2_def swap_def tp_def step_def)
  
  have vv: "v = [y,x]@c@[x]" using w2 dd v aa by auto

  from pref1 pref2 star w2 ende have
    "Tp [x, y] qs (OPT2 qs [x, y]) = 1 + length c div 2" unfolding assms(2) by auto
  also have "… = (length v div 2)" using vv star by auto
  finally show ?thesis .
qed

lemma OPT2_C1: assumes "x ≠ y" "qs ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
  shows "real (Tp [x,y] qs (OPT2 qs [x,y])) = (length qs - 1) / 2"
proof -
  from assms(2) have qs: "qs ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
    by(simp add: conc_assoc)
  have "(length qs) mod 2 = 1"
  proof -
    from assms(2) have "qs ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[x]}" by (simp add: conc_assoc)
    then obtain p q r where pqr: "qs=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[x]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[x]" by auto
    with pqr have a: "length qs = 3+length q" by auto
    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b show ?thesis by auto
  qed
  with OPT2_C[where u="[]", OF assms(1) _ _ qs] show ?thesis apply auto
      by (metis minus_mod_eq_div_mult [symmetric] of_nat_mult of_nat_numeral) 
qed  
  
lemma OPT2_C2: assumes "x ≠ y" "qs ∈ lang (seq[Atom x, Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])"
  shows "Tp [x,y] qs (OPT2 qs [x,y]) = ((length qs - 2) / 2)"
proof -
  from assms(2) obtain v where
      qsv: "qs = [x]@v" and vv: "v ∈ lang (seq[Atom y, Atom x, Star(Times (Atom y) (Atom x)), Atom x])" by (auto simp add: conc_def)
  have "(length v) mod 2 = 1"
  proof -
    from vv have "v ∈ ({[y]} @@ {[x]}) @@ star({[y]} @@ {[x]}) @@ {[x]}" by (simp add: conc_assoc)
    then obtain p q r where pqr: "v=p@q@r" and "p∈({[y]} @@ {[x]})"
              and q: "q ∈ star ({[y]} @@ {[x]})" and "r ∈{[x]}" by (metis concE)
    then have rr: "p = [y,x]" "r=[x]" by(auto simp add: conc_def)
    with pqr have a: "length v = 3+length q" by auto
    from q have b: "length q mod 2 = 0"
    apply(induct q rule: star_induct) by (auto)    
    from a b show ?thesis by auto
  qed
  with OPT2_C[where u="[x]", OF assms(1) qsv _ vv] qsv show ?thesis apply(auto)
      by (metis minus_mod_eq_div_mult [symmetric] of_nat_mult of_nat_numeral)     
qed 



lemma OPT2_ub: "set qs ⊆ {x,y} ⟹ Tp [x,y] qs (OPT2 qs [x,y]) ≤ length qs"
proof(induct qs arbitrary: x y)
  case (Cons q qs)
  then have "set qs ⊆ {x,y}" "q∈{x,y}" by auto
  note Cons1=Cons this
  show ?case
  proof (cases qs)
    case Nil
    with Cons1 show "Tp [x,y] (q # qs) (OPT2 (q # qs) [x,y]) ≤ length (q # qs)"
        apply(simp add: tp_def) by blast
  next
    case (Cons q' qs')
    with Cons1 have "q'∈{x,y}" by auto
    note Cons=Cons this

    from Cons1 Cons have T: "Tp [x, y] qs (OPT2 qs [x, y]) ≤ length qs"
                            "Tp [y, x] qs (OPT2 qs [y, x]) ≤ length qs" by auto
    show "Tp [x,y] (q # qs) (OPT2 (q # qs) [x,y]) ≤ length (q # qs)"
          unfolding Cons apply(simp only: OPT2.simps)
          apply(split if_splits(1))
            apply(safe)
            proof (goal_cases)
              case 1
              have "Tp [x, y] (x # q' # qs') ((0, []) # OPT2 (q' # qs') [x, y])
                      = tp [x, y] x (0,[]) + Tp [x, y] qs (OPT2 qs [x, y])"
                        by(simp add: step_def Cons)
              also have "… ≤ tp [x, y] x (0,[]) + length qs" using T by auto
              also have "… ≤ length (x # q' # qs')" using Cons by(simp add: tp_def)
              finally show ?case .
            next
              case 2
              with Cons1 Cons show ?case
                apply(split if_splits(1))
                apply(safe)
                proof (goal_cases)
                  case 1
                  then have "Tp [x, y] (y # x # qs') ((0, []) # OPT2 (x # qs') [x, y])
                          = tp [x, y] y (0,[]) + Tp [x, y] qs (OPT2 qs [x, y])"
                            by(simp add: step_def)
                  also have "… ≤ tp [x, y] y (0,[]) + length qs" using T by auto
                  also have "… ≤ length (y # x # qs')" using Cons by(simp add: tp_def)
                  finally show ?case .
                next
                  case 2
                  then have "Tp [x, y] (y # y # qs') ((1, []) # OPT2 (y # qs') [y, x])
                          = tp [x, y] y (1,[]) + Tp [y, x] qs (OPT2 qs [y, x])"
                            by(simp add: step_def mtf2_def swap_def)
                  also have "… ≤ tp [x, y] y (1,[]) + length qs" using T by auto
                  also have "… ≤ length (y # y # qs')" using Cons by(simp add: tp_def)
                  finally show ?case .
                qed
           qed
  qed
qed simp 

lemma OPT2_padded: "R∈{[x,y],[y,x]} ⟹ set qs ⊆ {x,y} 
      ⟹  Tp R (qs@[x,x]) (OPT2 (qs@[x,x]) R)
              ≤ Tp R (qs@[x]) (OPT2 (qs@[x]) R) + 1"
apply(induct qs arbitrary: R)
  apply(simp)
    apply(case_tac "R=[x,y]")
      apply(simp add: step_def tp_def )
      apply(simp add: step_def mtf2_def swap_def tp_def)
  proof (goal_cases)
    case (1 a qs R)
    then have a: "a ∈ {x,y}" by auto 
    with 1 show ?case
      apply(cases qs)
        apply(cases "a=x")
          apply(cases "R=[x,y]")
            apply(simp add: step_def tp_def)
            apply(simp add: step_def mtf2_def swap_def tp_def)
          apply(cases "R=[x,y]")
            apply(simp add: step_def tp_def)
            apply(simp add: step_def mtf2_def swap_def tp_def)
      proof (goal_cases)
        case (1 p ps)
        show ?case
          apply(cases "a=x")
            apply(cases "R=[x,y]")
              apply(simp add: OPT2x step_def) using 1 apply(simp)
              using 1(2) apply(simp)
                apply(cases qs)
                  apply(simp add: step_def mtf2_def swap_def tp_def)
                  using 1 by(auto simp add: swap_def mtf2_def step_def)
       qed
qed 


lemma  OPT2_split11:
  assumes xy: "x≠y"
  shows "R∈{[x,y],[y,x]} ⟹ set xs ⊆ {x,y} ⟹ set ys ⊆ {x,y} ⟹ OPT2 (xs@[x,x]@ys) R = OPT2 (xs@[x,x]) R @ OPT2 ys [x,y]"
proof (induct xs arbitrary: R)
  case Nil
  then show ?case
  apply(simp)
  apply(cases ys)
    apply(simp)
    apply(cases "R=[x,y]") 
      apply(simp)
      by(simp)
next
  case (Cons a as)
  note iH=this
  then have AS: "set as ⊆ {x,y}" and A: "a ∈ {x,y}" by auto
  note iH=Cons(1)[where R="[y,x]", simplified, OF AS Cons(4)]
  note iH'=Cons(1)[where R="[x,y]", simplified, OF AS Cons(4)]
  show ?case
  proof (cases "R=[x,y]")
    case True
    note R=this
    from iH iH' show ?thesis
    apply(cases "a=x")
      apply(simp add: R OPT2x)
      using A apply(simp)
      apply(cases as)
        apply(simp add: R)
        using AS apply(simp)
        apply(case_tac "aa=x")
          by(simp_all add: R)
  next
    case False
    with Cons(2) have R: "R=[y,x]" by auto
    from iH iH' show ?thesis
    apply(cases "a=y")
      apply(simp add: R OPT2x)
      using A apply(simp)
      apply(cases as)
        apply(simp add: R) 
        apply(case_tac "aa=y")
          by (simp_all add: R)
   qed  
qed  
 
subsection "The function steps" 
 
 
lemma steps_append: "length qs = length as ⟹ steps s (qs@[q]) (as@[a]) = step (steps s qs as) q a"
apply(induct qs as arbitrary: s rule: list_induct2) by simp_all
 
end