# Theory OPT2

theory OPT2
imports Partial_Cost_Model RExp_Var

section

theory OPT2
imports
Partial_Cost_Model
RExp_Var
begin

lemma
unfolding Inf_nat_def using LeastI[of ] by force

lemma nn_contains_Inf:
fixes S ::
assumes nn:
shows
using assms Inf_nat_def LeastI by force

subsection

fun OPT2 ::  where

|
|

lemma OPT2_length:
apply(induct σ arbitrary: x y)
apply(simp)
apply(case_tac σ) by(auto)

lemma OPT2x:
apply(cases σ') by (simp_all)

lemma swapOpt:
proof -
show ?thesis
proof (cases )
case True

have
unfolding T_opt_def
apply(rule nn_contains_Inf)
apply(auto) by (rule Ex_list_of_length)

then obtain asyx where costyx:
and lenyx:
unfolding T_opt_def by auto

from True lenyx have  by auto
then obtain A asyx' where aa:  using list.exhaust by blast
then obtain m1 a1 where AA:  by fastforce

let ?asxy =

from True obtain q σ' where qq:  using list.exhaust by blast

have t:
unfolding tp_def
apply(simp) unfolding swap_def by (simp)

have s:
unfolding step_def mtf2_def by(simp add: swap_def)

have T:  unfolding qq aa AA by(auto simp add: s t)

have l:  using T costyx by simp
have  using lenyx aa by auto
then have inside:  by force
then have b:  by auto

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

lemma tt:
apply(cases rest1) by(auto simp add: step_def mtf2_def swap_def)

lemma splitqsallg:
proof -
assume ne:
assume axy:
have
by(simp only: List.list.collapse[OF ne])
then show ?thesis by auto
qed

lemma splitqs:
proof -
assume axy:
have ne:  apply(cases rest1) by(simp_all)
have
by(simp only: List.list.collapse[OF ne])
also have
by(simp only: tt[OF axy])
also have  by(simp)
finally show ?thesis .
qed

lemma tpx:

lemma yup:

lemma swapsxy:
apply(induct sws)
apply(simp)
apply(simp) unfolding swap_def by auto

lemma mtf2xy:
by (metis mtf2_def swapsxy)

lemma stepxy: assumes
shows
unfolding step_def apply(simp only: split_def Let_def)
apply(rule mtf2xy)
apply(rule swapsxy) by fact+

subsection

lemma OPT2_is_lb:
proof (induct  arbitrary: x y σ rule: less_induct)
case (less)
show ?case
proof (cases σ)
case (Cons a σ')
note Cons1=Cons
show ?thesis unfolding Cons
proof(cases )
case True
from True Cons have qsform:  by auto
have up:
unfolding True
unfolding T_opt_def apply(rule cInf_greatest)
proof -
fix el
assume
then obtain Strat where lStrat:
and el:  by auto
then have ne:  by auto
let ?LA=

have  E0:   using yup by auto
also have E1:  by (simp add: OPT2x step_def)
also have E2:  apply(rule less(1)) using Cons less(2,3) by auto
also have
proof (cases )
case True
have aha:
unfolding T_opt_def apply(rule cInf_lower)
apply(auto) apply(rule exI[where x=]) using lStrat by auto

also have E4:
unfolding True by(simp)
also have E5:  using splitqsallg[of Strat x x y σ', OF ne, simplified]
by (auto)
finally show ?thesis by auto
next
case False
have tp1:
proof (rule ccontr)
let ?a =
assume
then have tp0:  by auto
then have  unfolding tp_def by(simp add: split_def)
then have nopaid:  by auto
have
unfolding step_def apply(simp add: split_def nopaid)
unfolding mtf2_def by(simp)
then show  using False by auto
qed

from False have yx:
using stepxy[where x=x and y=y and a=] by auto

have E3:  using swapOpt by auto
also have E4:
apply(simp) unfolding T_opt_def apply(rule cInf_lower)
apply(auto) apply(rule exI[where x=]) using lStrat by auto
also have E5:  using yx by auto
also have E6:  using tp1 by auto

also have E7:  using splitqsallg[of Strat x x y σ', OF ne, simplified]
by (auto)
finally show ?thesis by auto
qed
also have  using True el by simp
finally show  by auto
qed
then show
using True by simp
next

case False
with less Cons have ay:  by auto
show  unfolding ay
proof(cases σ')
case Nil
have up:
unfolding T_opt_def apply(rule cInf_greatest)
proof -
fix el
assume
then obtain Strat where Strat:  and
el:  by auto
from Strat obtain a where a:  by (metis Suc_length_conv length_0_conv)
show  unfolding el a apply(simp) unfolding tp_def apply(simp add: split_def)
apply(cases )
by(simp)
qed

show  unfolding Nil
apply(simp add: tp_def) using less(3) apply(simp)
using up by(simp)
next
case (Cons b rest2)

show up:
unfolding Cons
proof (cases )
case True

show
unfolding True
unfolding T_opt_def apply(rule cInf_greatest)
proof -
fix el
assume
then obtain Strat where lenStrat:  and
Strat:  by auto
have v:  using less(2)[unfolded Cons1 Cons] by auto

let ?L1 =
let ?L2 =

let ?a1 =
let ?a2 =
let ?r =

have  by (metis Nitpick.size_list_simp(2) Suc_length_conv lenStrat list.collapse list.discI list.inject)

have 1:
proof -
have a:  using lenStrat by auto
have b:  using lenStrat by (metis Nitpick.size_list_simp(2) Suc_length_conv list.discI list.inject)

have 1:
using splitqsallg[OF a, where a=y and x=x and y=y, simplified] by (simp)
have tt:
using stepxy[where A=] by blast

have 2:
apply(cases )
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
unfolding True
using less(3) by(simp add: tp_def step_def OPT2x)
also have  apply(simp)
apply(rule less(1))
apply(fact) by fact
also

have
proof (cases )
case True
have 2:  apply(simp)
unfolding T_opt_def apply(rule cInf_lower)
apply(simp) apply(rule exI[where x=]) by (auto simp: lenStrat)
have 3:  apply(simp)
proof -
have
apply(cases ) by (simp_all add: less(3))
then show  by auto
qed
from 1 2 3 True show ?thesis by auto
next
case False
note L2F=this
have L1:  apply(rule stepxy) by simp_all
have  apply(rule stepxy) using L1 by simp_all
with False have 2:  by auto

have k:  using 1 2 by auto

have l:
using less(3) unfolding tp_def apply(cases )

have r:
proof (cases )
case True
note T=this
then have  unfolding True
proof(cases )
case True
have  unfolding T  apply(simp add: split_def step_def)
unfolding True mtf2_def by(simp)
with L2F have  by auto
then show  ..
next
case False
then show
qed
with l have  by auto
with k show ?thesis by auto
next
case False
from L1 False have 2:  by auto
{ fix k sws T
have
apply(rule ccontr) by (simp add: less(3) mtf2_def)
}
have t1:  unfolding tp_def apply(simp add: split_def)
apply(cases ) using  by auto
have t2:  unfolding tp_def apply(simp add: split_def)
apply(cases ) using  by auto
have
by(rule k)
with t1 t2 2 show ?thesis by auto
qed
have t:
unfolding T_opt_def apply(rule cInf_lower)
apply(auto) apply(rule exI[where x=]) by(simp add: lenStrat)
show ?thesis
proof -
have
using  swapOpt by auto
also have  using t by auto
also have  using r by auto
finally show ?thesis .
qed

qed
also have  using Strat by auto
finally show  .
qed

next
case False
with Cons1 Cons less(2) have bisy:  by auto
with less(3) have  by simp
show
unfolding bisy
unfolding T_opt_def apply(rule cInf_greatest)
proof -
fix el
assume
then obtain Strat where lenStrat:  and
Strat:  by auto
have v:  using less(2)[unfolded Cons1 Cons] by auto

let ?L1 =
let ?L2 =

let ?a1 =
let ?a2 =
let ?r =

have  by (metis Nitpick.size_list_simp(2) Suc_length_conv lenStrat list.collapse list.discI list.inject)

have 1:
proof -
have a:  using lenStrat by auto
have b:  using lenStrat by (metis Nitpick.size_list_simp(2) Suc_length_conv list.discI list.inject)

have 1:
using splitqsallg[OF a, where a=y and x=x and y=y, simplified] by (simp)
have tt:
using stepxy[where A=] by blast

have 2:
apply(cases )
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
using less(3) by(simp add: tp_def step_def mtf2_def swap_def OPT2x)
also have  apply(simp)
apply(rule less(1))
using v less(3) by(auto)
also

have
proof (cases )
case True
have 2:  apply(simp)
unfolding T_opt_def apply(rule cInf_lower)
apply(simp) apply(rule exI[where x=]) by (auto simp: lenStrat)
have 3:  apply(simp)
proof -
have
apply(cases ) by (simp_all add: less(3))
then show  by auto
qed
from 1 2 3 True show ?thesis by auto
next
case False
note L2F=this
have L1:  apply(rule stepxy) by simp_all
have  apply(rule stepxy) using L1 by simp_all
with False have 2:  by auto

have k:  using 1 2 by auto

have l:
using less(3) unfolding tp_def apply(cases )

have r:
proof (cases )
case False
from L1 False have  by auto
note T=this
then have  unfolding T
apply(cases )
using  by auto
with l k show ?thesis by auto
next

case True
note T=this

have  unfolding T
proof(cases )
case True
have  unfolding T  apply(simp add: split_def step_def)
unfolding True mtf2_def by(simp)
with L2F have  by auto
then show  ..
next
case False
then show
qed
with l have  by auto
with k show ?thesis by auto

qed
have t:
unfolding T_opt_def apply(rule cInf_lower)
apply(auto) apply(rule exI[where x=]) by(simp add: lenStrat)
show ?thesis
proof -
have
using  swapOpt by auto
also have  using t by auto
also have  using r by auto
finally show ?thesis .
qed

qed
also have  using Strat by auto
finally show  .
qed
qed
qed
qed
qed

lemma OPT2_is_ub:
unfolding T_opt_def apply(rule cInf_lower)
apply(simp) apply(rule exI[where x=])

lemma OPT2_is_opt:
by (simp add: OPT2_is_lb OPT2_is_ub antisym)

subsection

lemma OPT2_A: assumes
shows
proof -
from assms(2) obtain u v where qs:  and u:  and v:  by (auto simp: conc_def)
from u have pref1:
apply(cases )
apply(simp)

have ende:  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
shows
using OPT2_A[OF assms] by simp

lemma OPT2_B: assumes
shows
proof -
from assms(3) have pref1:
apply(cases )
apply(simp)

from assms(4) obtain a w where v:  and  and w:  by(auto)
from this(2) have aa:  by(simp add: conc_def)

from assms(1) this v have pref2:

from w obtain c d where w2:  and c:  and d:  by auto
then have dd:  by auto

from c[simplified] have star:
proof(induct c rule: star_induct)
case (append r s)
then have r:  by auto
then have  by simp
also have
using assms(1) by(simp add: tp_def step_def OPT2x)
also have  using append by simp
also have  using r by auto
finally show ?case .
qed simp

have ende:  unfolding dd using assms(1) by(simp add: mtf2_def swap_def tp_def step_def)

have vv:  using w2 dd v aa by auto

from pref1 pref2 star w2 ende have
unfolding assms(2) by auto
also have  using vv by auto
finally show ?thesis .
qed

lemma OPT2_B1: assumes
shows
proof -
from assms(2) have qs:
have
proof -
from assms(2) have  by (simp add: conc_assoc)
then obtain p q r where pqr:  and
and q:  and  by (metis concE)
then have rr:   by auto
with pqr have a:  by auto
from q have b:
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
shows
proof -
from assms(2) obtain v where
qsv:  and vv:  by (auto simp add: conc_def)
have
proof -
from vv have  by (simp add: conc_assoc)
then obtain p q r where pqr:  and
and q:  and  by (metis concE)
then have rr:   by(auto simp add: conc_def)
with pqr have a:  by auto
from q have b:
apply(induct q rule: star_induct) by (auto)
from a b show ?thesis by auto
qed
with OPT2_B[where u=, OF assms(1) qsv _ vv] qsv show ?thesis by(auto)
qed

lemma OPT2_C: assumes
and
shows
proof -
from assms(3) have pref1:
apply(cases )
apply(simp)

from assms(4) obtain a w where v:  and aa:  and w:  by(auto simp: conc_def)

from assms(1) this v have pref2:

from w obtain c d where w2:  and c:  and d:  by auto
then have dd:  by auto

from c[simplified] have star:
proof(induct c rule: star_induct)
case (append r s)
from append have mod:  by simp
from append have r:  by auto
then have  by simp
also have
using assms(1) by(simp add: tp_def step_def OPT2x)
also have  using append by simp
also have  using r by auto
finally show ?case by(simp add: mod r)
qed simp

have ende:  unfolding dd using assms(1) by(simp add: mtf2_def swap_def tp_def step_def)

have vv:  using w2 dd v aa by auto

from pref1 pref2 star w2 ende have
unfolding assms(2) by auto
also have  using vv star by auto
finally show ?thesis .
qed

lemma OPT2_C1: assumes
shows
proof -
from assms(2) have qs:
have
proof -
from assms(2) have  by (simp add: conc_assoc)
then obtain p q r where pqr:  and
and q:  and  by (metis concE)
then have rr:   by auto
with pqr have a:  by auto
from q have b:
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
shows
proof -
from assms(2) obtain v where
qsv:  and vv:  by (auto simp add: conc_def)
have
proof -
from vv have  by (simp add: conc_assoc)
then obtain p q r where pqr:  and
and q:  and  by (metis concE)
then have rr:   by(auto simp add: conc_def)
with pqr have a:  by auto
from q have b:
apply(induct q rule: star_induct) by (auto)
from a b show ?thesis by auto
qed
with OPT2_C[where u=, 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:
proof(induct qs arbitrary: x y)
case (Cons q qs)
then have   by auto
note Cons1=Cons this
show ?case
proof (cases qs)
case Nil
with Cons1 show
next
case (Cons q' qs')
with Cons1 have  by auto
note Cons=Cons this

from Cons1 Cons have T:
by auto
show
unfolding Cons apply(simp only: OPT2.simps)
apply(split if_splits(1))
apply(safe)
proof (goal_cases)
case 1
have
also have  using T by auto
also have  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
also have  using T by auto
also have  using Cons by(simp add: tp_def)
finally show ?case .
next
case 2
then have
also have  using T by auto
also have  using Cons by(simp add: tp_def)
finally show ?case .
qed
qed
qed
qed simp

apply(induct qs arbitrary: R)
apply(simp)
apply(case_tac )
apply(simp add: step_def mtf2_def swap_def tp_def)
proof (goal_cases)
case (1 a qs R)
then have a:  by auto
with 1 show ?case
apply(cases qs)
apply(cases )
apply(cases )
apply(simp add: step_def mtf2_def swap_def tp_def)
apply(cases )
apply(simp add: step_def mtf2_def swap_def tp_def)
proof (goal_cases)
case (1 p ps)
show ?case
apply(cases )
apply(cases )
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:
shows
proof (induct xs arbitrary: R)
case Nil
then show ?case
apply(simp)
apply(cases ys)
apply(simp)
apply(cases )
apply(simp)
by(simp)
next
case (Cons a as)
note iH=this
then have AS:  and A:  by auto
note iH=Cons(1)[where R=, simplified, OF AS Cons(4)]
note iH'=Cons(1)[where R=, simplified, OF AS Cons(4)]
show ?case
proof (cases )
case True
note R=this
from iH iH' show ?thesis
apply(cases )
using A apply(simp)
apply(cases as)
using AS apply(simp)
apply(case_tac )
next
case False
with Cons(2) have R:  by auto
from iH iH' show ?thesis
apply(cases )
using A apply(simp)
apply(cases as)