(* Title: Phase Partitioning Author: Max Haslbeck *) 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 set_Lxx: "xs ∈ Lxx x y ⟹ set xs ⊆ {x,y}" unfolding Lxx_def L_lasthasxx_def apply(simp add: star_def) sle dgehammer *) 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]") (* FIXME why is simp_all needed? *) 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 (* with padding *) 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