Theory Phase_Partitioning
section "Phase Partitioning"
theory Phase_Partitioning
imports OPT2
begin
subsection "Definition of Phases"
definition "other a x y = (if a=x then y else x)"
definition Lxx where
"Lxx (x::nat) y = lang (L_lasthasxx x y)"
lemma Lxx_not_nullable: "[] ∉ Lxx x y"
unfolding Lxx_def L_lasthasxx_def by simp
lemma Lxx_ends_in_two_equal: "xs ∈ Lxx x y ⟹ ∃pref e. xs = pref @ [e,e]"
by(auto simp: conc_def Lxx_def L_lasthasxx_def)
lemma "Lxx x y = Lxx y x" unfolding Lxx_def by(rule lastxx_com)
definition "hideit x y = (Plus rexp.One (nodouble x y))"
lemma Lxx_othercase: "set qs ⊆ {x,y} ⟹ ¬ (∃xs ys. qs = xs @ ys ∧ xs ∈ Lxx x y) ⟹ qs ∈ lang (hideit x y)"
proof -
assume "set qs ⊆ {x,y}"
then have "qs ∈ lang (myUNIV x y)" using myUNIV_alle[of x y] by blast
then have "qs ∈ star (lang (L_lasthasxx x y)) @@ lang (hideit x y)" unfolding hideit_def
by(auto simp add: myUNIV_char)
then have qs: "qs ∈ star (Lxx x y) @@ lang (hideit x y)" by(simp add: Lxx_def)
assume notpos: "¬ (∃xs ys. qs = xs @ ys ∧ xs ∈ Lxx x y)"
show "qs ∈ lang (hideit x y)"
proof -
from qs obtain A B where qsAB: "qs=A@B" and A: "A∈star (Lxx x y)" and B: "B∈lang (hideit x y)" by auto
with notpos have notin: "A ∉ (Lxx x y)" by blast
from A have 1: "A = [] ∨ A ∈ (Lxx x y) @@ star (Lxx x y)" using Regular_Set.star_unfold_left by auto
have 2: "A ∉ (Lxx x y) @@ star (Lxx x y)"
proof (rule ccontr)
assume "¬ A ∉ Lxx x y @@ star (Lxx x y)"
then have " A ∈ Lxx x y @@ star (Lxx x y)" by auto
then obtain A1 A2 where "A=A1@A2" and A1: "A1∈(Lxx x y)" and "A2∈ star (Lxx x y)" by auto
with qsAB have "qs=A1@(A2@B)" "A1∈(Lxx x y)" by auto
with notpos have "A1 ∉ (Lxx x y)" by blast
with A1 show "False" by auto
qed
from 1 2 have "A=[]" by auto
with qsAB have "qs=B" by auto
with B show ?thesis by simp
qed
qed
fun pad where "pad xs x y = (if xs=[] then [x,x] else
(if last xs = x then xs @ [x] else xs @ [y]))"
lemma pad_adds2: "qs ≠ [] ⟹ set qs ⊆ {x,y} ⟹ pad qs x y = qs @ [last qs]"
apply(auto) by (metis insertE insert_absorb insert_not_empty last_in_set subset_iff)
lemma nodouble_padded: "qs ≠ [] ⟹ qs ∈ lang (nodouble x y) ⟹ pad qs x y ∈ Lxx x y"
proof -
assume nn: "qs ≠ []"
assume "qs ∈ lang (nodouble x y)"
then have a: "qs ∈ lang (seq
[Plus (Atom x) rexp.One,
Star (Times (Atom y) (Atom x)),
Atom y]) ∨ qs ∈ lang
(seq
[Plus (Atom y) rexp.One,
Star (Times (Atom x) (Atom y)),
Atom x])" unfolding nodouble_def by auto
show ?thesis
proof (cases "qs ∈ lang (seq [Plus (Atom x) One, Star (Times (Atom y) (Atom x)), Atom y])")
case True
then have "qs ∈ lang (seq [Plus (Atom x) One, Star (Times (Atom y) (Atom x))]) @@ {[y]}"
by(simp add: conc_assoc)
then have "last qs = y" by auto
with nn have p: "pad qs x y = qs @ [y]" by auto
have A: "pad qs x y ∈ lang (seq [Plus (Atom x) One, Star (Times (Atom y) (Atom x)),
Atom y]) @@ {[y]}" unfolding p
apply(simp)
apply(rule concI)
using True by auto
have B: "lang (seq [Plus (Atom x) One, Star (Times (Atom y) (Atom x)),
Atom y]) @@ {[y]} = lang (seq [Plus (Atom x) One, Star (Times (Atom y) (Atom x)),
Atom y, Atom y])" by (simp add: conc_assoc)
show "pad qs x y ∈ Lxx x y" unfolding Lxx_def L_lasthasxx_def
using B A by auto
next
case False
with a have T: "qs ∈ lang (seq [Plus (Atom y) One, Star (Times (Atom x) (Atom y)), Atom x])" by auto
then have "qs ∈ lang (seq [Plus (Atom y) One, Star (Times (Atom x) (Atom y))]) @@ {[x]}"
by(simp add: conc_assoc)
then have "last qs = x" by auto
with nn have p: "pad qs x y = qs @ [x]" by auto
have A: "pad qs x y ∈ lang (seq [Plus (Atom y) One, Star (Times (Atom x) (Atom y)),
Atom x]) @@ {[x]}" unfolding p
apply(simp)
apply(rule concI)
using T by auto
have B: "lang (seq [Plus (Atom y) One, Star (Times (Atom x) (Atom y)),
Atom x]) @@ {[x]} = lang (seq [Plus (Atom y) One, Star (Times (Atom x) (Atom y)),
Atom x, Atom x])" by (simp add: conc_assoc)
show "pad qs x y ∈ Lxx x y" unfolding Lxx_def L_lasthasxx_def
using B A by auto
qed
qed
thm UnE
lemma "c ∈ A ∪ B ⟹ P"
apply(erule UnE) oops
lemma LxxE: "qs ∈ Lxx x y
⟹ (qs ∈ lang (seq [Atom x, Atom x]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom x, Star (Times (Atom y) (Atom x)), Atom y, Atom y]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom x, Star (Times (Atom y) (Atom x)), Atom x]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom y]) ⟹ P x y qs)
⟹ P x y qs"
unfolding Lxx_def lastxx_is_4cases[symmetric] L_4cases_def apply(simp only: verund.simps lang.simps)
using UnE by blast
thm UnE LxxE
lemma "qs ∈ Lxx x y ⟹ P"
apply(erule LxxE) oops
lemma LxxI: "(qs ∈ lang (seq [Atom x, Atom x]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom x, Star (Times (Atom y) (Atom x)), Atom y, Atom y]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom x, Star (Times (Atom y) (Atom x)), Atom x]) ⟹ P x y qs)
⟹ (qs ∈ lang (seq [Plus (Atom x) rexp.One, Atom y, Atom y]) ⟹ P x y qs)
⟹ (qs ∈ Lxx x y ⟹ P x y qs)"
unfolding Lxx_def lastxx_is_4cases[symmetric] L_4cases_def apply(simp only: verund.simps lang.simps)
by blast
lemma Lxx1: "xs ∈ Lxx x y ⟹ length xs ≥ 2"
apply(rule LxxI[where P="(λx y qs. length qs ≥ 2)"])
apply(auto) by(auto simp: conc_def)
subsection "OPT2 Splitting"
lemma ayay: "length qs = length as ⟹ T⇩p s (qs@[q]) (as@[a]) = T⇩p s qs as + t⇩p (steps s qs as) q a"
apply(induct qs as arbitrary: s rule: list_induct2) by simp_all
lemma tlofOPT2: "Q ∈ {x,y} ⟹ set QS ⊆ {x,y} ⟹ R ∈ {[x, y], [y, x]} ⟹ tl (OPT2 ((Q # QS) @ [x, x]) R) =
OPT2 (QS @ [x, x]) (step R Q (hd (OPT2 ((Q # QS) @ [x, x]) R)))"
apply(cases "Q=x")
apply(cases "R=[x,y]")
apply(simp add: OPT2x step_def)
apply(simp)
apply(cases QS)
apply(simp add: step_def mtf2_def swap_def)
apply(simp add: step_def mtf2_def swap_def)
apply(cases "R=[x,y]")
apply(simp)
apply(cases QS)
apply(simp add: step_def mtf2_def swap_def)
apply(simp add: step_def mtf2_def swap_def)
by(simp add: OPT2x step_def)
lemma T⇩p_split: "length qs1=length as1 ⟹ T⇩p s (qs1@qs2) (as1@as2) = T⇩p s qs1 as1 + T⇩p (steps s qs1 as1) qs2 as2"
apply(induct qs1 as1 arbitrary: s rule: list_induct2) by(simp_all)
lemma T⇩p_spliting: "x≠y ⟹ set xs ⊆ {x,y} ⟹ set ys ⊆ {x,y} ⟹
R ∈ {[x,y],[y,x]} ⟹
T⇩p R (xs@[x,x]) (OPT2 (xs@[x,x]) R) + T⇩p [x,y] ys (OPT2 ys [x,y])
= T⇩p R (xs@[x,x]@ys) (OPT2 (xs@[x,x]@ys) R)"
proof -
assume nxy: "x≠y"
assume XSxy: "set xs ⊆ {x,y}"
assume YSxy: "set ys ⊆ {x,y}"
assume R: "R ∈ {[x,y],[y,x]}"
{
fix R
assume XSxy: "set xs ⊆ {x,y}"
have "R∈{[x,y],[y,x]} ⟹ set xs ⊆ {x,y} ⟹ steps R (xs@[x,x]) (OPT2 (xs@[x,x]) R) = [x,y]"
proof(induct xs arbitrary: R)
case Nil
then show ?case
apply(cases "R=[x,y]")
apply simp_all apply(simp add: step_def)
by(simp add: step_def mtf2_def swap_def)
next
case (Cons Q QS)
let ?R'="(step R Q (hd (OPT2 ((Q # QS) @ [x, x]) R)))"
have a: "Q ∈ {x,y}" and b: "set QS ⊆ {x,y}" using Cons by auto
have t: "?R' ∈ {[x,y],[y,x]}"
apply(rule stepxy) using nxy Cons by auto
then have "length (OPT2 (QS @ [x, x]) ?R') > 0"
apply(cases "?R' = [x,y]") by(simp_all add: OPT2_length)
then have "OPT2 (QS @ [x, x]) ?R' ≠ []" by auto
then have hdtl: "OPT2 (QS @ [x, x]) ?R' = hd (OPT2 (QS @ [x, x]) ?R') # tl (OPT2 (QS @ [x, x]) ?R')"
by auto
have maa: "(tl (OPT2 ((Q # QS) @ [x, x]) R)) = OPT2 (QS @ [x, x]) ?R' "
using tlofOPT2[OF a b Cons(2)] by auto
from Cons(2) have "length (OPT2 ((Q # QS) @ [x, x]) R) > 0"
apply(cases "R = [x,y]") by(simp_all add: OPT2_length)
then have nempty: "OPT2 ((Q # QS) @ [x, x]) R ≠ []" by auto
then have "steps R ((Q # QS) @ [x, x]) (OPT2 ((Q # QS) @ [x, x]) R)
= steps R ((Q # QS) @ [x, x]) (hd(OPT2 ((Q # QS) @ [x, x]) R) # tl(OPT2 ((Q # QS) @ [x, x]) R))"
by(simp)
also have "…
= steps ?R' (QS @ [x,x]) (tl (OPT2 ((Q # QS) @ [x, x]) R))"
unfolding maa by auto
also have "… = steps ?R' (QS @ [x,x]) (OPT2 (QS @ [x, x]) ?R')" using maa by auto
also with Cons(1)[OF t b] have "… = [x,y]" by auto
finally show ?case .
qed
} note aa=this
from aa XSxy R have ll: "steps R (xs@[x,x]) (OPT2 (xs@[x,x]) R)
= [x,y]" by auto
have uer: " length (xs @ [x, x]) = length (OPT2 (xs @ [x, x]) R)"
using R by (auto simp: OPT2_length)
have "OPT2 (xs @ [x, x] @ ys) R = OPT2 (xs @ [x, x]) R @ OPT2 ys [x, y]"
apply(rule OPT2_split11)
using nxy XSxy YSxy R by auto
then have "T⇩p R (xs@[x,x]@ys) (OPT2 (xs@[x,x]@ys) R)
= T⇩p R ((xs@[x,x])@ys) (OPT2 (xs @ [x, x]) R @ OPT2 ys [x, y])" by auto
also have "… = T⇩p R (xs@[x,x]) (OPT2 (xs @ [x, x]) R)
+ T⇩p [x,y] ys (OPT2 ys [x, y])"
using T⇩p_split[of "xs@[x,x]" "OPT2 (xs @ [x, x]) R" R ys "OPT2 ys [x, y]", OF uer, unfolded ll]
by auto
finally show ?thesis by simp
qed
lemma OPTauseinander: "x≠y ⟹ set xs ⊆ {x,y} ⟹ set ys ⊆ {x,y} ⟹
LTS ∈ {[x,y],[y,x]} ⟹ hd LTS = last xs ⟹
xs = (pref @ [hd LTS, hd LTS]) ⟹
T⇩p [x,y] xs (OPT2 xs [x,y]) + T⇩p LTS ys (OPT2 ys LTS)
= T⇩p [x,y] (xs@ys) (OPT2 (xs@ys) [x,y])"
proof -
assume nxy: "x≠y"
assume xsxy: "set xs ⊆ {x,y}"
assume ysxy: "set ys ⊆ {x,y}"
assume L: "LTS ∈ {[x,y],[y,x]}"
assume "hd LTS = last xs"
assume prefix: "xs = (pref @ [hd LTS, hd LTS])"
show ?thesis
proof (cases "LTS = [x,y]")
case True
show ?thesis unfolding True prefix
apply(simp)
apply(rule T⇩p_spliting[simplified])
using nxy xsxy ysxy prefix by auto
next
case False
with L have TT: "LTS = [y,x]" by auto
show ?thesis unfolding TT prefix
apply(simp)
apply(rule T⇩p_spliting[simplified])
using nxy xsxy ysxy prefix by auto
qed
qed
subsection "Phase Partitioning lemma"
theorem Phase_partitioning_general:
fixes P :: "(nat state * 'is) pmf ⇒ nat ⇒ nat list ⇒ bool"
and A :: "(nat state,'is,nat,answer) alg_on_rand"
assumes xny: "(x0::nat) ≠ y0"
and cpos: "(c::real)≥0"
and static: "set σ ⊆ {x0,y0}"
and initial: "P (map_pmf (%is. ([x0,y0],is)) (fst A [x0,y0])) x0 [x0,y0]"
and D: "⋀a b σ s. σ ∈ Lxx a b ⟹ a≠b ⟹ {a,b}={x0,y0} ⟹ P s a [x0,y0] ⟹ set σ ⊆ {a,b}
⟹ T_on_rand' A s σ ≤ c * T⇩p [a,b] σ (OPT2 σ [a,b]) ∧ P (config'_rand A s σ) (last σ) [x0,y0]"
shows "T⇩p_on_rand A [x0,y0] σ ≤ c * T⇩p_opt [x0,y0] σ + c"
proof -
{
fix x y s
have "x ≠ y ⟹ P s x [x0,y0] ⟹ set σ ⊆ {x,y} ⟹ {x,y}={x0,y0} ⟹ T_on_rand' A s σ ≤ c * T⇩p [x,y] σ (OPT2 σ [x,y]) + c"
proof (induction "length σ" arbitrary: σ x y s rule: less_induct)
case (less σ)
show ?case
proof (cases "∃xs ys. σ=xs@ys ∧ xs ∈ Lxx x y")
case True
then obtain xs ys where qs: "σ=xs@ys" and xsLxx: "xs ∈ Lxx x y" by auto
with Lxx1 have len: "length ys < length σ" by fastforce
from qs(1) less(4) have ysxy: "set ys ⊆ {x,y}" by auto
have xsset: "set xs ⊆ {x, y}" using less(4) qs by auto
from xsLxx Lxx1 have lxsgt1: "length xs ≥ 2" by auto
then have xs_not_Nil: "xs ≠ []" by auto
from D[OF xsLxx less(2) less(5) less(3) xsset]
have D1: "T_on_rand' A s xs ≤ c * T⇩p [x, y] xs (OPT2 xs [x, y])"
and inv: "P (config'_rand A s xs) (last xs) [x0, y0]" by auto
from xsLxx Lxx_ends_in_two_equal obtain pref e where "xs = pref @ [e,e]" by metis
then have endswithsame: "xs = pref @ [last xs, last xs]" by auto
let ?c' = "[last xs, other (last xs) x y]"
have setys: "set ys ⊆ {x,y}" using qs less by auto
have setxs: "set xs ⊆ {x,y}" using qs less by auto
have lxs: "last xs ∈ set xs" using xs_not_Nil by auto
from lxs setxs have lxsxy: "last xs ∈ {x,y}" by auto
from lxs setxs have otherxy: "other (last xs) x y ∈ {x,y}" by (simp add: other_def)
from less(2) have other_diff: "last xs ≠ other (last xs) x y" by(simp add: other_def)
have lo: "{last xs, other (last xs) x y} = {x0, y0}"
using lxsxy otherxy other_diff less(5) by force
have nextstate: "{[last xs, other (last xs) x y], [other (last xs) x y, last xs]}
= { [x,y],[y,x]}" using lxsxy otherxy other_diff by fastforce
have setys': "set ys ⊆ {last xs, other (last xs) x y}"
using setys lxsxy otherxy other_diff by fastforce
have c: "T_on_rand' A (config'_rand A s xs) ys
≤ c * T⇩p ?c' ys (OPT2 ys ?c') + c"
apply(rule less(1))
apply(fact len)
apply(fact other_diff)
apply(fact inv)
apply(fact setys')
by(fact lo)
have well: "T⇩p [x, y] xs (OPT2 xs [x, y]) + T⇩p ?c' ys (OPT2 ys ?c')
= T⇩p [x, y] (xs @ ys) (OPT2 (xs @ ys) [x, y])"
apply(rule OPTauseinander[where pref=pref])
apply(fact)+
using lxsxy other_diff otherxy apply(fastforce)
apply(simp)
using endswithsame by simp
have E0: "T_on_rand' A s σ
= T_on_rand' A s (xs@ys)" using qs by auto
also have E1: "… = T_on_rand' A s xs + T_on_rand' A (config'_rand A s xs) ys"
by (rule T_on_rand'_append)
also have E2: "… ≤ T_on_rand' A s xs + c * T⇩p ?c' ys (OPT2 ys ?c') + c"
using c by simp
also have E3: "… ≤ c * T⇩p [x, y] xs (OPT2 xs [x, y]) + c * T⇩p ?c' ys (OPT2 ys ?c') + c"
using D1 by simp
also have "… = c * (T⇩p [x,y] xs (OPT2 xs [x,y]) + T⇩p ?c' ys (OPT2 ys ?c')) + c"
using cpos apply(auto) by algebra
also have "… = c * (T⇩p [x,y] (xs@ys) (OPT2 (xs@ys) [x,y])) + c"
using well by auto
also have E4: "… = c * (T⇩p [x,y] σ (OPT2 σ [x,y])) + c"
using qs by auto
finally show ?thesis .
next
case False
note f1=this
from Lxx_othercase[OF less(4) this, unfolded hideit_def] have
nodouble: "σ = [] ∨ σ ∈ lang (nodouble x y)" by auto
show ?thesis
proof (cases "σ = []")
case True
then show ?thesis using cpos by simp
next
case False
from False nodouble have qsnodouble: "σ ∈ lang (nodouble x y)" by auto
let ?padded = "pad σ x y"
have padset: "set ?padded ⊆ {x, y}" using less(4) by(simp)
from False pad_adds2[of σ x y] less(4) obtain addum where ui: "pad σ x y = σ @ [last σ]" by auto
from nodouble_padded[OF False qsnodouble] have pLxx: "?padded ∈ Lxx x y" .
have E0: "T_on_rand' A s σ ≤ T_on_rand' A s ?padded"
proof -
have "T_on_rand' A s σ = sum (T_on_rand'_n A s σ) {..<length σ}"
by(rule T_on_rand'_as_sum)
also have "…
= sum (T_on_rand'_n A s (σ @ [last σ])) {..<length σ}"
proof(rule sum.cong, goal_cases)
case (2 t)
then have "t < length σ" by auto
then show ?case by(simp add: nth_append)
qed simp
also have "… ≤ T_on_rand' A s ?padded"
unfolding ui
apply(subst (2) T_on_rand'_as_sum) by(simp add: T_on_rand'_nn del: T_on_rand'.simps)
finally show ?thesis by auto
qed
also have E1: "… ≤ c * T⇩p [x,y] ?padded (OPT2 ?padded [x,y])"
using D[OF pLxx less(2) less(5) less(3) padset] by simp
also have E2: "… ≤ c * (T⇩p [x,y] σ (OPT2 σ [x,y]) + 1)"
proof -
from False less(2) obtain σ' x' y' where qs': "σ = σ' @ [x']" and x': "x' = last σ" "y'≠x'" "y' ∈{x,y}"
by (metis append_butlast_last_id insert_iff)
have tla: "last σ ∈ {x,y}" using less(4) False last_in_set by blast
with x' have grgr: "{x,y} = {x',y'}" by auto
then have "(x = x' ∧ y = y') ∨ (x = y' ∧ y = x')" using less(2) by auto
then have tts: "[x, y] ∈ {[x', y'], [y', x']}" by blast
from qs' ui have pd: "?padded = σ' @ [x', x']" by auto
have "T⇩p [x,y] (?padded) (OPT2 (?padded) [x,y])
= T⇩p [x,y] (σ' @ [x', x']) (OPT2 (σ' @ [x', x']) [x,y])"
unfolding pd by simp
also have gr: "…
≤ T⇩p [x,y] (σ' @ [x']) (OPT2 (σ' @ [x']) [x,y]) + 1"
apply(rule OPT2_padded[where x="x'" and y="y'"])
apply(fact)
using grgr qs' less(4) by auto
also have "… ≤ T⇩p [x,y] (σ) (OPT2 (σ) [x,y]) + 1"
unfolding qs' by simp
finally show ?thesis using cpos by (meson mult_left_mono of_nat_le_iff)
qed
also have "… = c * T⇩p [x,y] σ (OPT2 σ [x,y]) + c" by (metis (no_types, lifting) mult.commute of_nat_1 of_nat_add semiring_normalization_rules(2))
finally show ?thesis .
qed
qed
qed
} note allg=this
have "T_on_rand A [x0,y0] σ ≤ c * real (T⇩p [x0, y0] σ (OPT2 σ [x0, y0])) + c"
apply(rule allg)
apply(fact)
using initial apply(simp add: map_pmf_def)
apply(fact assms(3))
by simp
also have "… = c * T⇩p_opt [x0, y0] σ + c"
using OPT2_is_opt[OF assms(3,1)] by(simp)
finally show ?thesis .
qed
term "A::(nat,'is) alg_on"
theorem Phase_partitioning_general_det:
fixes P :: "(nat state * 'is) ⇒ nat ⇒ nat list ⇒ bool"
and A :: "(nat,'is) alg_on"
assumes xny: "(x0::nat) ≠ y0"
and cpos: "(c::real)≥0"
and static: "set σ ⊆ {x0,y0}"
and initial: "P ([x0,y0],(fst A [x0,y0])) x0 [x0,y0]"
and D: "⋀a b σ s. σ ∈ Lxx a b ⟹ a≠b ⟹ {a,b}={x0,y0} ⟹ P s a [x0,y0] ⟹ set σ ⊆ {a,b}
⟹ T_on' A s σ ≤ c * T⇩p [a,b] σ (OPT2 σ [a,b]) ∧ P (config' A s σ) (last σ) [x0,y0]"
shows "T⇩p_on A [x0,y0] σ ≤ c * T⇩p_opt [x0,y0] σ + c"
proof -
thm Phase_partitioning_general
thm T_deter_rand
term T_on'
term "embed"
show ?thesis oops
end