theory Complexity_Framework
imports
QTRS.Complexity
QTRS.Q_Relative_Rewriting
TA.Multihole_Context
begin
context
fixes Cp FS F :: "'f sig"
begin
inductive_set Fsharp_terms :: "('f, 'v) term set"
where
Fsharp_term:
"(f, length ts) ∈ FS ⟹ (⋀ t. t ∈ set ts ⟹ funas_term t ⊆ F) ⟹ Fun f ts ∈ Fsharp_terms"
lemma Fsharp_terms_imp_is_Fun [dest, simp]:
assumes "t ∈ Fsharp_terms"
shows "is_Fun t"
using assms by (cases) simp
inductive is_DP_complexity :: "('f, 'v) trs ⇒ ('f, 'v) trs ⇒ ('f, 'v) complexity_measure ⇒ bool"
where
is_DP_complexity: "wf_trs RS ⟹ wf_trs R ⟹
funas_trs R ⊆ F ⟹
lhss RS ⊆ Fsharp_terms ⟹
(⋀ l r. (l, r) ∈ RS ⟹ ∃ C ts. r =⇩f (C, ts) ∧ funas_mctxt C ⊆ Cp ∧ set ts ⊆ Fsharp_terms) ⟹
FS ∩ Cp = {} ⟹ FS ∩ F = {} ⟹ Cp ∩ F = {} ⟹
(case cm of Runtime_Complexity C D ⇒ set C ⊆ F ∧ set D ⊆ FS ∪ Cp | _ ⇒ False) ⟹
is_DP_complexity RS R cm"
inductive_set Tsharp_terms :: "('f, 'v) term set"
where
base: "funas_term t ⊆ F ⟹ t ∈ Tsharp_terms" |
sharp: "t ∈ Fsharp_terms ⟹ t ∈ Tsharp_terms" |
compound: "(f, length ts) ∈ Cp ⟹ (⋀ t. t ∈ set ts ⟹ t ∈ Tsharp_terms) ⟹ Fun f ts ∈ Tsharp_terms"
context
fixes RS R :: "('f, 'v) trs" and cm :: "('f, 'v) complexity_measure"
assumes is_DP': "is_DP_complexity RS R cm"
begin
lemmas DP = is_DP' [unfolded is_DP_complexity.simps, simplified]
lemma terms_of_Tsharp_terms: "terms_of cm ⊆ Tsharp_terms"
proof -
from DP obtain C D where cm: "cm = Runtime_Complexity C D" by (cases cm, auto)
with DP have C: "set C ⊆ F" and D: "set D ⊆ FS ∪ Cp" by auto
{
fix t
assume "t ∈ terms_of cm"
from this[unfolded cm] C D
obtain f ts where t: "t = Fun f ts" and f: "(f, length ts) ∈ FS ∪ Cp" and
args: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ F"
by (force simp: funas_args_term_def simp del: Un_iff)
let ?f = "(f,length ts)"
from f have "t ∈ Tsharp_terms"
proof
assume f: "?f ∈ FS"
show ?thesis unfolding t
by (rule sharp, rule Fsharp_term[OF f args])
next
assume f: "?f ∈ Cp"
show ?thesis unfolding t
by (rule compound[OF f base[OF args]])
qed
}
thus ?thesis by auto
qed
lemma qrstep_Tsharp_terms:
assumes step: "(s,t) ∈ qrstep nfs Q (RS ∪ R)"
and sT: "s ∈ Tsharp_terms"
shows "t ∈ Tsharp_terms"
proof -
note DP = DP[unfolded is_DP_complexity.simps, simplified]
from DP have wf: "wf_trs (RS ∪ R)" by (auto simp: wf_trs_def)
note funas_term_subst[simp]
from step have "(s,t) ∈ rstep (RS ∪ R)" by auto
from sT this show ?thesis
proof (induct s arbitrary: t)
case (base s t) note IH = this
from rstepE[OF IH(2)] obtain C l r σ where lr: "(l,r) ∈ RS ∪ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" .
from IH(1)[unfolded s] have lF: "funas_term l ⊆ F" by auto
from wf_trs_imp_lhs_Fun[OF wf lr] obtain f ls where l: "l = Fun f ls" by auto
with lF DP have f: "(f,length ls) ∉ FS" by auto
from lr have "(l,r) ∈ R"
proof
assume "(l,r) ∈ RS"
with DP have "l ∈ Fsharp_terms" by auto
from this l f show ?thesis by (cases, auto)
qed
with s t have "(s,t) ∈ rstep R" by auto
from rstep_preserves_funas_terms[OF _ IH(1) this] DP have "funas_term t ⊆ F" by auto
thus ?case ..
next
case (compound f ss) note IH = this
from rstepE[OF IH(4)] obtain C l r σ where lr: "(l,r) ∈ RS ∪ R" and s: "Fun f ss = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" .
from wf_trs_imp_lhs_Fun[OF wf lr] obtain g ls where l: "l = Fun g ls" by auto
let ?g = "(g,length ls)"
from lr DP have "funas_term l ⊆ F ∨ l ∈ Fsharp_terms" by (cases, (force simp: funas_trs_def funas_rule_def)+)
hence "?g ∈ F ∨ ?g ∈ FS"
proof
assume "l ∈ Fsharp_terms"
thus ?thesis unfolding l by (cases, auto)
qed (simp add: l)
with DP have g: "?g ∉ Cp" by auto
with s l IH(1) obtain bef D aft where C: "C = More f bef D aft" by (cases C, auto)
with lr have step: "(D⟨l ⋅ σ⟩, D⟨r ⋅ σ⟩) ∈ rstep (RS ∪ R)" by auto
from s[unfolded C] have ss: "ss = bef @ D ⟨l ⋅ σ⟩ # aft" by auto
hence "D⟨l ⋅ σ⟩ ∈ set ss" by auto
from IH(3)[OF this step] have rec: "D⟨r ⋅ σ⟩ ∈ Tsharp_terms" by auto
show ?case unfolding t C ctxt_apply_term.simps
by (rule Tsharp_terms.compound, insert IH(1-2) rec, auto simp: ss)
next
case (sharp s t) note IH = this
from rstepE[OF IH(2)] obtain C l r σ where lr: "(l,r) ∈ RS ∪ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" .
from IH(1)[unfolded s] have lF: "C⟨l ⋅ σ⟩ ∈ Fsharp_terms" by auto
from wf_trs_imp_lhs_Fun[OF wf lr] obtain f ls where l: "l = Fun f ls" by auto
let ?f = "(f,length ls)"
show ?case
proof (cases C)
case (More g bef D aft) note C = this
let ?g = "(g,Suc (length bef + length aft))"
from lF[unfolded C] have DF: "funas_term (D ⟨l ⋅ σ⟩) ⊆ F" and g: "?g ∈ FS"
and b_a: "⋀ t. t ∈ set bef ∪ set aft ⟹ funas_term t ⊆ F" by (cases, force)+
with l DP have f: "(f,length ls) ∉ FS" by auto
from lr have lr: "(l,r) ∈ R"
proof
assume "(l,r) ∈ RS"
with DP have "l ∈ Fsharp_terms" by auto
from this l f show ?thesis by (cases, auto)
qed
from rstep_preserves_funas_terms[OF _ DF rstepI[OF lr refl refl]] DP
have DF: "funas_term (D⟨r ⋅ σ⟩) ⊆ F" by auto
have "t ∈ Fsharp_terms" unfolding t C ctxt_apply_term.simps
by (rule Fsharp_term, insert g DF b_a, force+)
thus ?thesis ..
next
case Hole note C = this
from C lF have lF: "l ⋅ σ ∈ Fsharp_terms" by simp
from this[unfolded l] DP have f: "?f ∉ F" by (cases, auto)
from lr have lr: "(l,r) ∈ RS"
proof
assume "(l,r) ∈ R"
with l DP have "?f ∈ F" unfolding funas_trs_def funas_rule_def[abs_def] by force
with f show ?thesis by auto
qed
with DP obtain D ts where r: "r =⇩f (D, ts)" and D: "funas_mctxt D ⊆ Cp" and
ts: "set ts ⊆ Fsharp_terms" by blast
from lF[unfolded l] have "Fun f (map (λt. t ⋅ σ) ls) ∈ Fsharp_terms" by simp
hence li: "⋀ li. li ∈ set ls ⟹ funas_term (li ⋅ σ) ⊆ F" by (cases, force+)
{
fix x
assume "x ∈ vars_term r"
with lr wf[unfolded wf_trs_def]
have "x ∈ vars_term l" by auto
with l obtain li where "li ∈ set ls" and "x ∈ vars_term li" by auto
with li[of li] have "funas_term (σ x) ⊆ F" by auto
} note σ = this
def τ ≡ "λ x. if x ∈ vars_term r then σ x else Var x"
have rτ: "r ⋅ σ = r ⋅ τ"
by (rule term_subst_eq, auto simp: τ_def)
have τ: "⋀ x. funas_term (τ x) ⊆ F" using σ
by (auto simp: τ_def)
def tss ≡ "map (λti. ti ⋅ τ) ts"
def r' ≡ "r ⋅ σ"
from subst_apply_mctxt_sound[OF r, of τ] have rsig: "r ⋅ σ =⇩f (D ⋅mc τ, tss)" unfolding rτ tss_def .
{
fix t'
assume "t' ∈ set tss"
then obtain t where tts: "t ∈ set ts" and t': "t' = t ⋅ τ" unfolding tss_def by auto
with ts have "t ∈ Fsharp_terms" by auto
then obtain f us where t: "t = Fun f us" and f: "(f,length us) ∈ FS"
and us: "⋀ u. u ∈ set us ⟹ funas_term u ⊆ F" by (cases, auto)
{
fix u
assume u: "u ∈ set us"
from us[OF u] have uF: "funas_term u ⊆ F" by auto
with τ have "funas_term (u ⋅ τ) ⊆ F" by auto
} note us = this
with f have "t' ∈ Fsharp_terms" unfolding t' t subst_apply_term.simps
by (intro Fsharp_term, force+)
}
hence "set tss ⊆ Fsharp_terms" by auto
with D rsig have "r ⋅ σ ∈ Tsharp_terms" unfolding r'_def[symmetric]
proof (induct D arbitrary: r' tss)
case (MHole r tss)
note eq = eqfE[OF MHole(2)]
from eq obtain t where tss: "tss = [t]" by (cases tss, auto)
with eq have "r = t" by auto
with MHole(3) tss show ?case by (auto intro: Tsharp_terms.sharp)
next
case (MVar x r tss)
note eq = eqfE[OF MVar(2)]
from eq have "r = τ x" by simp
with τ[of x] show ?case by (auto intro: Tsharp_terms.base)
next
case (MFun f Ds r tss)
let ?n = "length Ds"
from MFun(3) have "r =⇩f (MFun f (map (λ D. D ⋅mc τ) Ds), tss)" by auto
from eqf_MFunE[OF this]
obtain rs sss where
r: "r = Fun f rs"
and len: "length rs = ?n"
"length sss = ?n"
and rec: "⋀i. i < ?n ⟹ rs ! i =⇩f (Ds ! i ⋅mc τ, sss ! i)"
and tss: "tss = concat sss" by auto
{
fix i
assume i: "i < ?n"
hence mem: "Ds ! i ∈ set Ds" by auto
with MFun(2) have Cp: "funas_mctxt (Ds ! i) ⊆ Cp" by auto
from i len have "sss ! i ∈ set sss" by auto
with tss have "set (sss ! i) ⊆ set tss" by auto
with MFun(4) have "set (sss ! i) ⊆ Fsharp_terms" by auto
from MFun(1)[OF mem Cp rec[OF i] this] have "rs ! i ∈ Tsharp_terms" .
}
with len have IH: "set rs ⊆ Tsharp_terms" unfolding set_conv_nth by auto
from MFun(2) len have "(f,length rs) ∈ Cp" by auto
from Tsharp_terms.compound[OF this] IH have "Fun f rs ∈ Tsharp_terms" by auto
with r show ?case by simp
qed
thus ?thesis unfolding t C by simp
qed
qed
qed
lemma avanzini_14_20:
"(qrstep nfs Q (RS ∪ R))^* `` Tsharp_terms ⊆ Tsharp_terms"
"(qrstep nfs Q (RS ∪ R))^* `` terms_of cm ⊆ Tsharp_terms"
proof -
let ?R = "qrstep nfs Q (RS ∪ R)" let ?T = "Tsharp_terms"
{
fix t
assume "t ∈ ?R^* `` ?T"
then obtain s where s: "s ∈ ?T" and st: "(s,t) ∈ ?R^*" by auto
from st have "t ∈ ?T"
proof (induct)
case base
show ?case by (rule s)
next
case (step t v)
from qrstep_Tsharp_terms[OF step(2-3)] show ?case .
qed
}
thus one: "?R^* `` ?T ⊆ ?T" by auto
from one terms_of_Tsharp_terms show "?R^* `` terms_of cm ⊆ ?T" by blast
qed
end
end
end