Theory OPT2
section "OPT2"
theory OPT2
imports
Partial_Cost_Model
RExp_Var
begin
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: "T⇩p_opt [x,y] σ ≤ 1 + T⇩p_opt [y,x] σ"
proof -
show ?thesis
proof (cases "length σ > 0")
case True
have "T⇩p_opt [y,x] σ ∈ {T⇩p [y, x] σ as |as. length as = length σ}"
unfolding T_opt_def
apply(rule Inf_nat_def1)
apply(auto) by (rule Ex_list_of_length)
then obtain asyx where costyx: "T⇩p [y,x] σ asyx = T⇩p_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: "t⇩p [x, y] q (m1, a1@[0]) = Suc (t⇩p [y, x] q (m1, a1))"
unfolding t⇩p_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: "T⇩p [x,y] σ ?asxy = 1 + T⇩p [y,x] σ asyx" unfolding qq aa AA by(auto simp add: s t)
have l: "1 + T⇩p_opt [y,x] σ = T⇩p [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: "T⇩p [x, y] σ ?asxy ∈ {T⇩p [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} ⟹
t⇩p [x, y] a (hd (Strat)) +
(let L=step [x,y] a (hd (Strat))
in T⇩p L (rest1) (tl Strat)) = T⇩p [x, y] (a # rest1) Strat"
proof -
assume ne: "Strat ≠ []"
assume axy: "a ∈ {x,y}"
have "T⇩p [x, y] (a # rest1) (Strat)
= T⇩p [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} ⟹ T⇩p [x, y] (a # rest1) (OPT2 (a # rest1) [x, y])
= t⇩p [x, y] a (hd (OPT2 (a # rest1) [x, y])) +
(let L=step [x,y] a (hd (OPT2 (a # rest1) [x, y]))
in T⇩p 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 "T⇩p [x, y] (a # rest1) (OPT2 (a # rest1) [x, y])
= T⇩p [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 "… = T⇩p [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 "… = t⇩p [x, y] a (hd (OPT2 (a # rest1) [x, y])) +
(let L=step [x,y] a (hd (OPT2 (a # rest1) [x, y]))
in T⇩p L (rest1) (OPT2 (rest1) L))" by(simp)
finally show ?thesis .
qed
lemma tpx: "t⇩p [x, y] x (hd (OPT2 (x # rest1) [x, y])) = 0"
by (simp add: OPT2x t⇩p_def)
lemma yup: "T⇩p [x, y] (x # rest1) (OPT2 (x # rest1) [x, y])
= (let L=step [x,y] x (hd (OPT2 (x # rest1) [x, y]))
in T⇩p 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 ⟹ T⇩p [x,y] σ (OPT2 σ [x,y]) ≤ T⇩p_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 True
from True Cons have qsform: "σ = x#σ'" by auto
have up: "T⇩p [x, y] (x # σ') (OPT2 (x # σ') [x, y]) ≤ T⇩p_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 ∈ {T⇩p [x, y] (x # σ') as |as. length as = length (x # σ')}"
then obtain Strat where lStrat: "length Strat = length (x # σ')"
and el: "T⇩p [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: "T⇩p [x, y] (x # σ') (OPT2 (x # σ') [x, y])
=T⇩p ?LA (σ') (OPT2 (σ') ?LA)" using yup by auto
also have E1: "… = T⇩p [x,y] (σ') (OPT2 (σ') [x,y])" by (simp add: OPT2x step_def)
also have E2: "… ≤ T⇩p_opt [x,y] σ'" apply(rule less(1)) using Cons less(2,3) by auto
also have "… ≤ T⇩p [x, y] (x # σ') Strat"
proof (cases "(step [x, y] x (hd Strat)) = [x,y]")
case True
have aha: "T⇩p_opt [x, y] σ' ≤ T⇩p [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: "… ≤ t⇩p [x, y] x (hd Strat) + T⇩p (step [x, y] x (hd Strat)) σ' (tl Strat)"
unfolding True by(simp)
also have E5: "… = T⇩p [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: "t⇩p [x, y] x (hd Strat) ≥ 1"
proof (rule ccontr)
let ?a = "hd Strat"
assume "¬ 1 ≤ t⇩p [x, y] x ?a"
then have tp0: "t⇩p [x, y] x ?a = 0" by auto
then have "size (snd ?a) = 0" unfolding t⇩p_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: "T⇩p_opt [x, y] σ' ≤ 1 + T⇩p_opt [y, x] σ'" using swapOpt by auto
also have E4: "… ≤ 1 + T⇩p [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 + T⇩p (step [x, y] x (hd Strat)) σ' (tl Strat)" using yx by auto
also have E6: "… ≤ t⇩p [x, y] x (hd Strat) + T⇩p (step [x, y] x (hd Strat)) σ' (tl Strat)" using tp1 by auto
also have E7: "… = T⇩p [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 "T⇩p [x, y] (x # σ') (OPT2 (x # σ') [x, y]) ≤ el" by auto
qed
then show "T⇩p [x, y] (a # σ') (OPT2 (a # σ') [x, y]) ≤ T⇩p_opt [x, y] (a # σ')"
using True by simp
next
case False
with less Cons have ay: "a=y" by auto
show "T⇩p [x, y] (a # σ') (OPT2 (a # σ') [x, y]) ≤ T⇩p_opt [x, y] (a # σ')" unfolding ay
proof(cases σ')
case Nil
have up: "T⇩p_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 ∈ {T⇩p [x, y] [y] as |as. length as = length [y]}"
then obtain Strat where Strat: "length Strat = length [y]" and
el: "el = T⇩p [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 t⇩p_def apply(simp add: split_def)
apply(cases "snd a")
apply(simp add: less(3))
by(simp)
qed
show "T⇩p [x, y] (y # σ') (OPT2 (y # σ') [x, y]) ≤ T⇩p_opt [x, y] (y # σ')" unfolding Nil
apply(simp add: t⇩p_def) using less(3) apply(simp)
using up by(simp)
next
case (Cons b rest2)
show up: "T⇩p [x, y] (y # σ') (OPT2 (y # σ') [x, y]) ≤ T⇩p_opt [x, y] (y # σ')"
unfolding Cons
proof (cases "b=x")
case True
show "T⇩p [x, y] (y # b # rest2) (OPT2 (y # b # rest2) [x, y]) ≤ T⇩p_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 ∈ {T⇩p [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 = T⇩p [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)))"
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: "T⇩p [x, y] (y # x # rest2) Strat
= t⇩p [x, y] y (hd Strat) + t⇩p ?L1 x (hd (tl Strat))
+ T⇩p ?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: "T⇩p [x, y] (y # x # rest2) Strat
= t⇩p [x, y] y (hd Strat) + T⇩p ?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: "T⇩p ?L1 (x # rest2) (tl Strat) = t⇩p ?L1 x (hd (tl Strat)) + T⇩p ?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 " T⇩p [x, y] (y # x # rest2) (OPT2 (y # x # rest2) [x, y])
= 1 + T⇩p [x, y] (rest2) (OPT2 (rest2) [x, y])"
unfolding True
using less(3) by(simp add: t⇩p_def step_def OPT2x)
also have "… ≤ 1 + T⇩p_opt [x, y] (rest2)" apply(simp)
apply(rule less(1))
apply(simp add: less(2) Cons1 Cons)
apply(fact) by fact
also
have "… ≤ T⇩p [x, y] (y # x # rest2) Strat"
proof (cases "?L2 = [x,y]")
case True
have 2: "t⇩p [x, y] y (hd Strat) + t⇩p ?L1 x (hd (tl Strat))
+ T⇩p [x,y] rest2 (tl (tl Strat)) ≥ t⇩p [x, y] y (hd Strat) + t⇩p ?L1 x (hd (tl Strat))
+ T⇩p_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: "t⇩p [x, y] y (hd Strat) + t⇩p ?L1 x (hd (tl Strat))
+ T⇩p_opt [x,y] rest2 ≥ 1 + T⇩p_opt [x,y] rest2" apply(simp)
proof -
have "t⇩p [x, y] y (hd Strat) ≥ 1"
unfolding t⇩p_def apply(simp add: split_def)
apply(cases "snd (hd Strat)") by (simp_all add: less(3))
then show "Suc 0 ≤ t⇩p [x, y] y (hd Strat) + t⇩p ?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: "T⇩p [x, y] (y # x # rest2) Strat
= t⇩p [x, y] y (hd Strat) + t⇩p ?L1 x (hd (tl Strat)) +
T⇩p [y,x] rest2 (tl (tl Strat))" using 1 2 by auto
have l: "t⇩p [x, y] y (hd Strat) > 0"
using less(3) unfolding t⇩p_def apply(cases "snd (hd Strat) = []")
by (simp_all add: split_def)
have r: "T⇩p [x, y] (y # x # rest2) Strat ≥ 2 + T⇩p [y,x] rest2 (tl (tl Strat))"
proof (cases "?L1 = [x,y]")
case True
note T=this
then have "t⇩p ?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 < t⇩p [x, y] x (hd (tl Strat))" ..
next
case False
then show "0 < t⇩p [x, y] x (hd (tl Strat))"
unfolding t⇩p_def by(simp add: split_def)
qed
with l have " t⇩p [x, y] y (hd Strat) + t⇩p ?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: "t⇩p [x, y] y (hd Strat) ≥ 1" unfolding t⇩p_def apply(simp add: split_def)
apply(cases "(snd (hd Strat))") using ‹x ≠ y› by auto
have t2: "t⇩p [y,x] x (hd (tl Strat)) ≥ 1" unfolding t⇩p_def apply(simp add: split_def)
apply(cases "(snd (hd (tl Strat)))") using ‹x ≠ y› by auto
have "T⇩p [x, y] (y # x # rest2) Strat
= t⇩p [x, y] y (hd Strat) + t⇩p (step [x, y] y (hd Strat)) x (hd (tl Strat)) + T⇩p [y, x] rest2 (tl (tl Strat))"
by(rule k)
with t1 t2 2 show ?thesis by auto
qed
have t: "T⇩p [y, x] rest2 (tl (tl Strat)) ≥ T⇩p_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 + T⇩p_opt [x, y] rest2 ≤ 2 + T⇩p_opt [y, x] rest2"
using swapOpt by auto
also have "… ≤ 2 + T⇩p [y, x] rest2 (tl (tl Strat))" using t by auto
also have "… ≤ T⇩p [x, y] (y # x # rest2) Strat" using r by auto
finally show ?thesis .
qed
qed
also have "… = el" using Strat by auto
finally show "T⇩p [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 "T⇩p [x, y] (y # b # rest2) (OPT2 (y # b # rest2) [x, y]) ≤ T⇩p_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 ∈ {T⇩p [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 = T⇩p [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)))"
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: "T⇩p [x, y] (y # y # rest2) Strat
= t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat))
+ T⇩p ?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: "T⇩p [x, y] (y # y # rest2) Strat
= t⇩p [x, y] y (hd Strat) + T⇩p ?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: "T⇩p ?L1 (y # rest2) (tl Strat) = t⇩p ?L1 y (hd (tl Strat)) + T⇩p ?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 " T⇩p [x, y] (y # y # rest2) (OPT2 (y # y # rest2) [x, y])
= 1 + T⇩p [y, x] (rest2) (OPT2 (rest2) [y, x])"
using less(3) by(simp add: t⇩p_def step_def mtf2_def swap_def OPT2x)
also have "… ≤ 1 + T⇩p_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 "… ≤ T⇩p [x, y] (y # y # rest2) Strat"
proof (cases "?L2 = [y,x]")
case True
have 2: "t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat))
+ T⇩p [y,x] rest2 (tl (tl Strat)) ≥ t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat))
+ T⇩p_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: "t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat))
+ T⇩p_opt [y,x] rest2 ≥ 1 + T⇩p_opt [y,x] rest2" apply(simp)
proof -
have "t⇩p [x, y] y (hd Strat) ≥ 1"
unfolding t⇩p_def apply(simp add: split_def)
apply(cases "snd (hd Strat)") by (simp_all add: less(3))
then show "Suc 0 ≤ t⇩p [x, y] y (hd Strat) + t⇩p ?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: "T⇩p [x, y] (y # y # rest2) Strat
= t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat)) +
T⇩p [x,y] rest2 (tl (tl Strat))" using 1 2 by auto
have l: "t⇩p [x, y] y (hd Strat) > 0"
using less(3) unfolding t⇩p_def apply(cases "snd (hd Strat) = []")
by (simp_all add: split_def)
have r: "T⇩p [x, y] (y # y # rest2) Strat ≥ 2 + T⇩p [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 "t⇩p ?L1 y (hd (tl Strat)) > 0" unfolding T
unfolding t⇩p_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 "t⇩p ?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 < t⇩p [y, x] y (hd (tl Strat))" ..
next
case False
then show "0 < t⇩p [y, x] y (hd (tl Strat))"
unfolding t⇩p_def by(simp add: split_def)
qed
with l have " t⇩p [x, y] y (hd Strat) + t⇩p ?L1 y (hd (tl Strat)) ≥ 2" by auto
with k show ?thesis by auto
qed
have t: "T⇩p [x, y] rest2 (tl (tl Strat)) ≥ T⇩p_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 + T⇩p_opt [y, x] rest2 ≤ 2 + T⇩p_opt [x, y] rest2"
using swapOpt by auto
also have "… ≤ 2 + T⇩p [x, y] rest2 (tl (tl Strat))" using t by auto
also have "… ≤ T⇩p [x, y] (y # y # rest2) Strat" using r by auto
finally show ?thesis .
qed
qed
also have "… = el" using Strat by auto
finally show "T⇩p [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 ⟹ T⇩p [x,y] qs (OPT2 qs [x,y]) ≥ T⇩p_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 ⟹ T⇩p [x,y] qs (OPT2 qs [x,y]) = T⇩p_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 "T⇩p [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: "T⇩p [x,y] (u@v) (OPT2 (u@v) [x,y]) = T⇩p [x,y] v (OPT2 v [x,y])"
apply(cases "u=[]")
apply(simp)
by(simp add: OPT2x t⇩p_def step_def)
have ende: "T⇩p [x,y] v (OPT2 v [x,y]) = 1" unfolding v using assms(1) by(simp add: mtf2_def swap_def t⇩p_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 (T⇩p [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 "T⇩p [x,y] qs (OPT2 qs [x,y]) = (length v div 2)"
proof -
from assms(3) have pref1: "T⇩p [x,y] (u@v) (OPT2 (u@v) [x,y]) = T⇩p [x,y] v (OPT2 v [x,y])"
apply(cases "u=[]")
apply(simp)
by(simp add: OPT2x t⇩p_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: "T⇩p [x,y] v (OPT2 v [x,y]) = 1 + T⇩p [x,y] w (OPT2 w [x,y])"
by(simp add: t⇩p_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: "T⇩p [x,y] (c@d) (OPT2 (c@d) [x,y]) = (length c div 2) + T⇩p [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 "T⇩p [x, y] ((r @ s) @ d) (OPT2 ((r @ s) @ d) [x, y]) = T⇩p [x, y] ([y,x] @ (s @ d)) (OPT2 ([y,x] @ (s @ d)) [x, y])" by simp
also have "… = 1 + T⇩p [x, y] (s @ d) (OPT2 (s @ d) [x, y])"
using assms(1) by(simp add: t⇩p_def step_def OPT2x)
also have "… = 1 + length s div 2 + T⇩p [x, y] d (OPT2 d [x, y])" using append by simp
also have "… = length (r @ s) div 2 + T⇩p [x, y] d (OPT2 d [x, y])" using r by auto
finally show ?case .
qed simp
have ende: "T⇩p [x,y] d (OPT2 d [x,y]) = 1" unfolding dd using assms(1) by(simp add: mtf2_def swap_def t⇩p_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
"T⇩p [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 (T⇩p [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 "T⇩p [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 "T⇩p [x,y] qs (OPT2 qs [x,y]) = (length v div 2)"
proof -
from assms(3) have pref1: "T⇩p [x,y] (u@v) (OPT2 (u@v) [x,y]) = T⇩p [x,y] v (OPT2 v [x,y])"
apply(cases "u=[]")
apply(simp)
by(simp add: OPT2x t⇩p_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: "T⇩p [x,y] v (OPT2 v [x,y]) = 1 + T⇩p [x,y] w (OPT2 w [x,y])"
by(simp add: t⇩p_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: "T⇩p [x,y] (c@d) (OPT2 (c@d) [x,y]) = (length c div 2) + T⇩p [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 "T⇩p [x, y] ((r @ s) @ d) (OPT2 ((r @ s) @ d) [x, y]) = T⇩p [x, y] ([y,x] @ (s @ d)) (OPT2 ([y,x] @ (s @ d)) [x, y])" by simp
also have "… = 1 + T⇩p [x, y] (s @ d) (OPT2 (s @ d) [x, y])"
using assms(1) by(simp add: t⇩p_def step_def OPT2x)
also have "… = 1 + length s div 2 + T⇩p [x, y] d (OPT2 d [x, y])" using append by simp
also have "… = length (r @ s) div 2 + T⇩p [x, y] d (OPT2 d [x, y])" using r by auto
finally show ?case by(simp add: mod r)
qed simp
have ende: "T⇩p [x,y] d (OPT2 d [x,y]) = 0" unfolding dd using assms(1) by(simp add: mtf2_def swap_def t⇩p_def step_def)
have vv: "v = [y,x]@c@[x]" using w2 dd v aa by auto
from pref1 pref2 star w2 ende have
"T⇩p [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 (T⇩p [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 "T⇩p [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} ⟹ T⇩p [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 "T⇩p [x,y] (q # qs) (OPT2 (q # qs) [x,y]) ≤ length (q # qs)"
apply(simp add: t⇩p_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: "T⇩p [x, y] qs (OPT2 qs [x, y]) ≤ length qs"
"T⇩p [y, x] qs (OPT2 qs [y, x]) ≤ length qs" by auto
show "T⇩p [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 "T⇩p [x, y] (x # q' # qs') ((0, []) # OPT2 (q' # qs') [x, y])
= t⇩p [x, y] x (0,[]) + T⇩p [x, y] qs (OPT2 qs [x, y])"
by(simp add: step_def Cons)
also have "… ≤ t⇩p [x, y] x (0,[]) + length qs" using T by auto
also have "… ≤ length (x # q' # qs')" using Cons by(simp add: t⇩p_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 "T⇩p [x, y] (y # x # qs') ((0, []) # OPT2 (x # qs') [x, y])
= t⇩p [x, y] y (0,[]) + T⇩p [x, y] qs (OPT2 qs [x, y])"
by(simp add: step_def)
also have "… ≤ t⇩p [x, y] y (0,[]) + length qs" using T by auto
also have "… ≤ length (y # x # qs')" using Cons by(simp add: t⇩p_def)
finally show ?case .
next
case 2
then have "T⇩p [x, y] (y # y # qs') ((1, []) # OPT2 (y # qs') [y, x])
= t⇩p [x, y] y (1,[]) + T⇩p [y, x] qs (OPT2 qs [y, x])"
by(simp add: step_def mtf2_def swap_def)
also have "… ≤ t⇩p [x, y] y (1,[]) + length qs" using T by auto
also have "… ≤ length (y # y # qs')" using Cons by(simp add: t⇩p_def)
finally show ?case .
qed
qed
qed
qed simp
lemma OPT2_padded: "R∈{[x,y],[y,x]} ⟹ set qs ⊆ {x,y}
⟹ T⇩p R (qs@[x,x]) (OPT2 (qs@[x,x]) R)
≤ T⇩p 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 t⇩p_def )
apply(simp add: step_def mtf2_def swap_def t⇩p_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 t⇩p_def)
apply(simp add: step_def mtf2_def swap_def t⇩p_def)
apply(cases "R=[x,y]")
apply(simp add: step_def t⇩p_def)
apply(simp add: step_def mtf2_def swap_def t⇩p_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 t⇩p_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