section ‹Complexity›
theory Complexity
imports
TRS.Term_More
Show.Show_Instances
Jordan_Normal_Form.Derivation_Bound
Auxx.Shows_Literal
begin
subsection ‹Derivation Height and Complexity Functions›
locale traditional_complexity =
fixes r :: "('a::size) rel"
begin
abbreviation "DH x ≡ {n. ∃y. (x, y) ∈ r ^^ n}"
end
locale fb_sn =
fixes r :: "('a::size) rel"
assumes fb: "⋀x. finite {y. (x, y) ∈ r}" and sn: "SN r"
begin
interpretation traditional_complexity r .
lemma finite_DH:
"finite (DH x)"
using sn
proof (induct)
case (IH x)
let ?Y = "⋃y ∈ {y. (x, y) ∈ r}. Suc ` DH y"
have "DH x = {0} ∪ ?Y"
by (auto simp: relpow_commute elim: relpow_E2 intro!: rev_image_eqI)
(metis relcomp.relcompI relpow_commute)
moreover have "finite ?Y"
using fb and IH by simp
ultimately show ?case by simp
qed
end
context traditional_complexity
begin
definition "dh x = Max (DH x)"
abbreviation "CP n T ≡ {dh x | x. x ∈ T ∧ size x ≤ n}"
definition "cp n T = Max (CP n T)"
abbreviation "of_size A n ≡ {x ∈ A. size x ≤ n}"
end
datatype complexity_class = Comp_Poly nat
fun complexity_of :: "complexity_class ⇒ (nat ⇒ nat) set"
where
"complexity_of (Comp_Poly d) = { λ n. c * n ^ d + e | c e. True}"
lemma complexity_poly_mono_deg:
assumes "d ≤ d'"
and "f ∈ complexity_of (Comp_Poly d)"
shows "∃ g ∈ complexity_of (Comp_Poly d'). ∀ n. f n ≤ g n"
proof -
from assms obtain c e where f: "f = (λ n. c * n ^ d + e)" by auto
let ?g = "λ n. c * n ^ d' + e"
define g where "g ≡ λn. ?g n + c"
{
fix n
have "f n ≤ ?g n + c"
proof (cases n)
case 0
then show ?thesis by (cases d) (simp_all add: f)
next
case (Suc m)
have "f n ≤ ?g n"
using power_increasing [OF ‹d ≤ d'›, of n] by (auto simp: f Suc)
then show ?thesis by auto
next
qed
}
then have "∀ n. f n ≤ g n" by (simp add: g_def)
moreover have "g ∈ complexity_of (Comp_Poly d')"
by (auto simp: g_def) (rule exI [of _ c], rule exI [of _ "e + c"], auto)
ultimately show ?thesis by auto
qed
lemma complexity_poly_mono:
assumes "f ∈ complexity_of (Comp_Poly d)"
and "n ≤ m"
shows "f n ≤ f m"
using power_mono [OF ‹n ≤ m›, of d] and assms by auto
definition O_of :: "complexity_class ⇒ (nat ⇒ nat) set"
where
"O_of cl = {f. ∃ g ∈ complexity_of cl. ∀ n. f n ≤ g n}"
lemma O_of_polyI [intro]:
assumes ge: "⋀ n. f n ≤ c * n ^ d + e"
shows "f ∈ O_of (Comp_Poly d)"
using assms by (auto simp: O_of_def)
lemma O_of_poly_mono_deg:
assumes "d ≤ d'"
shows "O_of (Comp_Poly d) ⊆ O_of (Comp_Poly d')"
proof
fix f
assume "f ∈ O_of (Comp_Poly d)"
then obtain g where "g ∈ complexity_of (Comp_Poly d)" and "⋀ n. f n ≤ g n"
by (auto simp: O_of_def)
moreover with complexity_poly_mono_deg [OF ‹d ≤ d'›]
obtain h where "h ∈ complexity_of (Comp_Poly d')" and "⋀ n. g n ≤ h n" by blast
ultimately show "f ∈ O_of (Comp_Poly d')" unfolding O_of_def using le_trans by blast
qed
lemma O_of_poly_mono_deg_inv:
assumes subset: "O_of (Comp_Poly d1) ⊆ O_of (Comp_Poly d2)"
shows "d1 ≤ d2"
proof (rule ccontr)
assume "¬ d1 ≤ d2"
then have d: "d1 > d2" by simp
let ?f = "λ n :: nat. n ^ d1"
have "?f ∈ O_of (Comp_Poly d1)"
by (rule O_of_polyI [of _ 1 _ 0]) simp
with subset have "?f ∈ O_of (Comp_Poly d2)" by auto
then obtain g where g: "g ∈ complexity_of (Comp_Poly d2)"
and comp: "⋀ n. ?f n ≤ g n" by (auto simp: O_of_def)
from g obtain c e where g: "g = (λn. c * n ^ d2 + e)" by auto
from d obtain d where d1: "d1 = Suc d" and d: "d ≥ d2" by (cases d1) auto
define n where "n = c + e + 1"
have "n ≥ 1" by (auto simp: n_def)
then have nd1: "n ^ d2 ≥ 1" by simp
have "g n = c * n ^ d2 + e" by (simp add: g)
also have "… < c * n ^ d2 + e + 1" by simp
also have "e ≤ e * n ^ d2" using nd1 by simp
also have "1 ≤ 1 * n ^ d2" using nd1 by simp
finally have "g n < c * n ^ d2 + e * n ^ d2 + 1 * n ^ d2" by arith
also have "… = n * n ^ d2" by (simp add: n_def field_simps)
also have "… ≤ n * n^d" using power_increasing [OF d ‹n ≥ 1›] by simp
also have "… = ?f n" by (simp add: d1)
also have "… ≤ g n" using comp [of n] .
finally show False by auto
qed
lemma O_of_sum:
assumes f1: "f1 ∈ O_of cc"
and f2: "f2 ∈ O_of cc"
shows "(λ n. f1 n + f2 n) ∈ O_of cc"
proof (cases cc)
case (Comp_Poly d)
from f1 obtain c1 e1 where b1: "⋀ n. f1 n ≤ c1 * n ^ d + e1" by (auto simp: Comp_Poly O_of_def)
from f2 obtain c2 e2 where b2: "⋀ n. f2 n ≤ c2 * n ^ d + e2" by (auto simp: Comp_Poly O_of_def)
show ?thesis
proof (unfold Comp_Poly, rule O_of_polyI)
fix n
have "f1 n + f2 n ≤ c1 * n ^ d + e1 + c2 * n ^ d + e2"
using b1 [of n] and b2 [of n] by auto
also have "… = (c1 + c2) * n ^ d + (e1 + e2)" by (simp add: field_simps)
finally show "f1 n + f2 n ≤ (c1 + c2) * n ^ d + (e1 + e2)" .
qed
qed
fun degree :: "complexity_class ⇒ nat"
where
"degree (Comp_Poly d) = d"
instantiation complexity_class :: ord
begin
fun less_eq_complexity_class where "less_eq_complexity_class (x :: complexity_class) (y :: complexity_class) = (degree x ≤ degree y)"
fun less_complexity_class where "less_complexity_class (x :: complexity_class) (y :: complexity_class) = (degree x < degree y)"
instance ..
end
instantiation complexity_class :: showl
begin
definition "showsl_complexity_class (c::complexity_class) =
(if degree c = 0 then showsl_lit (STR ''O(1)'')
else if degree c = 1 then showsl_lit (STR ''O(n)'')
else showsl_lit (STR ''O(n^'') ∘ showsl (degree c) ∘ showsl_lit (STR '')''))"
definition "showsl_list (xs :: complexity_class list) = default_showsl_list showsl xs"
instance ..
end
lemma degree_subset [simp]:
"(cc ≤ cc') = (O_of cc ⊆ O_of cc')"
proof -
obtain d where cc: "cc = Comp_Poly d" by (cases cc) auto
obtain d' where cc': "cc' = Comp_Poly d'" by (cases cc') auto
show ?thesis
using O_of_poly_mono_deg O_of_poly_mono_deg_inv by (auto simp: cc cc')
qed
declare less_eq_complexity_class.simps [simp del]
definition deriv_bound_rel :: "'a rel ⇒ (nat ⇒ 'a set) ⇒ (nat ⇒ nat) ⇒ bool"
where
"deriv_bound_rel r as f ⟷ (∀ n a. a ∈ as n ⟶ deriv_bound r a (f n))"
context fb_sn
begin
interpretation traditional_complexity r .
text ‹@{const cp} is a derivation bound, whenever it is defined.›
lemma deriv_bound_rel_cp:
assumes fin: "⋀n. finite (CP n T)"
shows "deriv_bound_rel r (of_size T) (λn. cp n T)"
proof (unfold deriv_bound_rel_def, intro allI impI)
fix x and n
assume x: "x ∈ of_size T n"
show "deriv_bound r x (cp n T)"
proof
fix y and m
assume "cp n T < m" and "(x, y) ∈ r ^^ m"
then have "dh x ≥ m"
using finite_DH [of x] by (auto simp: dh_def) (metis Max_ge mem_Collect_eq)
then have "cp n T ≥ m"
using x and fin [of n]
by (auto simp: cp_def) (metis (mono_tags, lifting) Max_ge mem_Collect_eq order_trans)
with ‹cp n T < m› show False by arith
qed
qed
text ‹@{const cp} is a lower bound for any derivation bound, whenever it is defined.›
lemma cp_lower:
assumes "⋀x. DH x ≠ {}"
and "⋀n. finite (CP n T)"
and "⋀n. CP n T ≠ {}"
and db: "deriv_bound_rel r (of_size T) f"
shows "f n ≥ cp n T"
proof (rule ccontr)
assume "¬ cp n T ≤ f n"
then have "cp n T > f n" by arith
have *: "⋀x. x ∈ of_size T n ⟹ deriv_bound r x (f n)"
using db by (auto simp: deriv_bound_rel_def)
define m where "m = cp n T"
have **: "⋀k. k ∈ CP n T ⟹ k ≤ m"
using ‹finite (CP n T)› by (auto simp: m_def cp_def)
have "m ∈ CP n T"
using Max_in [OF ‹finite (CP n T)› ‹CP n T ≠ {}›] by (simp add: m_def cp_def)
then obtain x where "x ∈ of_size T n" and "dh x = m" by blast
then have "dh x > f n" by (simp add: m_def) (rule ‹cp n T > f n›)
moreover then obtain y where "(x, y) ∈ r ^^ dh x"
using Max_in [OF finite_DH ‹DH x ≠ {}›] by (auto simp: dh_def)
ultimately show False using * [OF ‹x ∈ of_size T n›] by (auto elim: deriv_boundE)
qed
end
lemma deriv_bound_rel_empty [simp]:
"deriv_bound_rel {} as f"
by (simp add: deriv_bound_rel_def)
definition deriv_bound_rel_class :: "'a rel ⇒ (nat ⇒ 'a set) ⇒ complexity_class ⇒ bool"
where
"deriv_bound_rel_class r as cpx ⟷ (∃ f. f ∈ O_of cpx ∧ deriv_bound_rel r as f)"
lemma deriv_bound_rel_class_polyI [intro]:
assumes "⋀ n a. a ∈ as n ⟹ deriv_bound r a (c * n ^ d + e)"
shows "deriv_bound_rel_class r as (Comp_Poly d)"
using assms unfolding deriv_bound_rel_class_def
by (intro exI [of _ "λ n. c * n ^ d + e"] conjI [OF O_of_polyI [OF le_refl]])
(auto simp: deriv_bound_rel_def)
lemma deriv_bound_rel_class_empty [simp]:
"deriv_bound_rel_class {} as cpx"
proof (cases cpx)
case (Comp_Poly d)
show ?thesis
unfolding deriv_bound_rel_class_def Comp_Poly
by (rule exI, rule conjI, rule O_of_polyI [OF le_refl], simp)
qed
lemma deriv_bound_relto_class_union:
assumes s1: "deriv_bound_rel_class (relto s1 (w ∪ s2)) as cc"
and s2: "deriv_bound_rel_class (relto s2 (w ∪ s1)) as cc"
shows "deriv_bound_rel_class (relto (s1 ∪ s2) w) as cc"
proof -
let ?r1 = "relto s1 (w ∪ s2)"
let ?r2 = "relto s2 (w ∪ s1)"
let ?r = "relto (s1 ∪ s2) w"
from s1[unfolded deriv_bound_rel_class_def]
obtain f1 where f1: "f1 ∈ O_of cc" and b1: "deriv_bound_rel ?r1 as f1" by auto
from s2[unfolded deriv_bound_rel_class_def]
obtain f2 where f2: "f2 ∈ O_of cc" and b2: "deriv_bound_rel ?r2 as f2" by auto
obtain f where f: "f = (λ n. f1 n + f2 n)" by auto
have fcc: "f ∈ O_of cc" using O_of_sum[OF f1 f2] unfolding f .
show ?thesis unfolding deriv_bound_rel_class_def
proof(intro exI conjI, rule fcc)
show "deriv_bound_rel ?r as f"
unfolding deriv_bound_rel_def
proof (intro allI impI)
fix n a
assume a: "a ∈ as n"
from b1[unfolded deriv_bound_rel_def] a
have b1: "deriv_bound ?r1 a (f1 n)" by simp
from b2[unfolded deriv_bound_rel_def] a
have b2: "deriv_bound ?r2 a (f2 n)" by simp
show "deriv_bound ?r a (f n)"
unfolding deriv_bound_def
proof
assume "∃ b. (a,b) ∈ ?r ^^ Suc (f n)"
then obtain b where ab: "(a,b) ∈ ?r ^^ Suc (f n)" by blast
from ab[unfolded relpow_fun_conv] obtain as where
as0: "as 0 = a"
and steps: "⋀ i. i < Suc (f n) ⟹ (as i, as (Suc i)) ∈ ?r" by auto
{
fix i
assume "i < Suc (f n)"
from steps[OF this]
obtain b c where asb: "(as i, b) ∈ w^*" and bc: "(b,c) ∈ s1 ∪ s2" and cas: "(c,as (Suc i)) ∈ w^*" by auto
let ?p = "(as i, as (Suc i))"
{
fix s
have "(as i, b) ∈ (w ∪ s)^*"
by (rule set_mp[OF _ asb], regexp)
} note asb = this
{
fix s
have "(c, as (Suc i)) ∈ (w ∪ s)^*"
by (rule set_mp[OF _ cas], regexp)
} note cas = this
from bc
have "?p ∈ ?r1 ∧ ?p ∈ (w ∪ s1)^* ∨ ?p ∈ ?r2 ∧ ?p ∈ (w ∪ s2)^*"
proof
assume bc: "(b,c) ∈ s1"
have s: "?p ∈ ?r1" using asb[of s2] bc cas[of s2] by auto
have ns: "?p ∈ (w ∪ s1)^* O (w ∪ s1) O (w ∪ s1)^* " using asb[of s1] bc cas[of s1] by auto
have "?p ∈ (w ∪ s1)^*" by (rule set_mp[OF _ ns], regexp)
with s show ?thesis by blast
next
assume bc: "(b,c) ∈ s2"
have s: "?p ∈ ?r2" using asb[of s1] bc cas[of s1] by auto
have ns: "?p ∈ (w ∪ s2)^* O (w ∪ s2) O (w ∪ s2)^* " using asb[of s2] bc cas[of s2] by auto
have "?p ∈ (w ∪ s2)^*" by (rule set_mp[OF _ ns], regexp)
with s show ?thesis by blast
qed
} note steps = this
{
fix i
assume i: "i ≤ Suc (f n)"
let ?p = "λ i i1 i2 b1 b2. (a,b1) ∈ ?r1 ^^ i1 ∧ (b1,as i) ∈ (w ∪ s2)^* ∧ (a,b2) ∈ ?r2 ^^ i2 ∧ (b2,as i) ∈ (w ∪ s1)^* ∧ i1 + i2 = i"
from i have "∃ i1 i2 b1 b2. ?p i i1 i2 b1 b2"
proof (induct i)
case 0
show ?case
proof (intro exI)
show "?p 0 0 0 a a" unfolding as0 by simp
qed
next
case (Suc i)
from Suc(2) have "i ≤ Suc (f n)" by simp
from Suc(1)[OF this] obtain i1 i2 b1 b2 where p: "?p i i1 i2 b1 b2" by blast
then have ab1: "(a,b1) ∈ ?r1 ^^ i1"
and b1ai: "(b1,as i) ∈ (w ∪ s2)^*"
and ab2: "(a,b2) ∈ ?r2 ^^ i2"
and b2ai: "(b2,as i) ∈ (w ∪ s1)^*"
and i: "i = i1 + i2" by auto
let ?a = "(as i, as (Suc i))"
from Suc(2) have "i < Suc (f n)" by simp
from steps[OF this] show ?case
proof
assume "?a ∈ ?r1 ∧ ?a ∈ (w ∪ s1)^*"
then have s: "?a ∈ ?r1" and ns: "?a ∈ (w ∪ s1)^*" by auto
from b1ai s have s: "(b1, as (Suc i)) ∈ (w ∪ s2)^* O ?r1" by blast
have "(b1, as (Suc i)) ∈ ?r1"
by (rule set_mp[OF _ s], regexp)
from relpow_Suc_I[OF ab1 this]
have s: "(a, as (Suc i)) ∈ ?r1 ^^ Suc i1" .
from b2ai ns have ns: "(b2, as (Suc i)) ∈ (w ∪ s1)^*" by auto
have "?p (Suc i) (Suc i1) i2 (as (Suc i)) b2" using s ns i ab2 by auto
then show ?thesis by blast
next
assume one: "?a ∈ ?r2 ∧ ?a ∈ (w ∪ s2)^*"
then have s: "?a ∈ ?r2" and ns: "?a ∈ (w ∪ s2)^*" by auto
from b2ai s have s: "(b2, as (Suc i)) ∈ (w ∪ s1)^* O ?r2" by blast
have "(b2, as (Suc i)) ∈ ?r2"
by (rule set_mp[OF _ s], regexp)
from relpow_Suc_I[OF ab2 this]
have s: "(a, as (Suc i)) ∈ ?r2 ^^ Suc i2" .
from b1ai ns have ns: "(b1, as (Suc i)) ∈ (w ∪ s2)^*" by auto
have "?p (Suc i) i1 (Suc i2) b1 (as (Suc i))" using s ns i ab1 by auto
then show ?thesis by blast
qed
qed
then have "∃ i1 i2 b1 b2. (a,b1) ∈ ?r1 ^^ i1 ∧ (a,b2) ∈ ?r2 ^^ i2 ∧ i1 + i2 = i" by blast
}
from this[OF le_refl]
obtain i1 i2 b1 b2 where steps1: "(a,b1) ∈ ?r1 ^^ i1" and steps2: "(a,b2) ∈ ?r2 ^^ i2" and i: "i1 + i2 = Suc (f n)" by blast
from deriv_bound_steps[OF steps1 b1] deriv_bound_steps[OF steps2 b2] have "i1 + i2 ≤ f1 n + f2 n" by simp
with i[unfolded f] show False by simp
qed
qed
qed
qed
datatype ('f, 'v) complexity_measure =
Derivational_Complexity "('f × nat) list" |
Runtime_Complexity "('f × nat) list" "('f × nat) list"
fun term_size :: "('f,'v)term ⇒ nat" where
"term_size (Var x) = Suc 0"
| "term_size (Fun f ts) = Suc (sum_list (map term_size ts))"
lemma term_size_map_funs_term [simp]:
"term_size (map_funs_term fg t) = term_size t"
proof (induct t)
case (Fun f ts)
then show ?case by (induct ts) auto
qed simp
lemma term_size_subst: "term_size t ≤ term_size (t ⋅ σ)"
proof (induct t)
case (Var x)
then show ?case by (cases "σ x") auto
next
case (Fun f ss)
then show ?case
by (induct ss, force+)
qed
lemma term_size_const_subst[simp]: "term_size (t ⋅ (λ _ . Fun f [])) = term_size t"
proof (induct t)
case (Fun f ts)
then show ?case by (induct ts, auto)
qed simp
lemma supt_term_size:
"s ⊳ t ⟹ term_size s > term_size t"
proof (induct rule: supt.induct)
case (arg s ss)
then show ?case by (induct ss, auto)
next
case (subt s ss t f)
then show ?case by (induct ss, auto)
qed
fun terms_of_nat :: "('f, 'v) complexity_measure ⇒ nat ⇒ ('f, 'v) terms"
where
"terms_of_nat (Derivational_Complexity F) n = {t. funas_term t ⊆ set F ∧ term_size t ≤ n}" |
"terms_of_nat (Runtime_Complexity C D) n =
{t. is_Fun t ∧ the (root t) ∈ set D ∧ funas_args_term t ⊆ set C ∧ term_size t ≤ n}"
fun terms_of :: "('f, 'v) complexity_measure ⇒ ('f, 'v) terms"
where
"terms_of (Derivational_Complexity F) = {t. funas_term t ⊆ set F}" |
"terms_of (Runtime_Complexity C D) =
{t. is_Fun t ∧ the (root t) ∈ set D ∧ funas_args_term t ⊆ set C}"
lemma terms_of:
"terms_of cm = ⋃(range (terms_of_nat cm))"
by (cases cm) auto
definition
deriv_bound_measure_class ::
"('f, 'v) term rel ⇒ ('f, 'v) complexity_measure ⇒ complexity_class ⇒ bool"
where
"deriv_bound_measure_class r cm cpx = deriv_bound_rel_class r (terms_of_nat cm) cpx"
lemma deriv_bound_measure_class_empty [simp]:
"deriv_bound_measure_class {} cm cc"
unfolding deriv_bound_measure_class_def by simp
lemma deriv_bound_measure_class_SN_on:
assumes bound: "deriv_bound_measure_class r cm p"
shows "SN_on r (terms_of cm)"
proof -
{
fix t
assume "t ∈ terms_of cm"
then obtain n where t: "t ∈ terms_of_nat cm n" unfolding terms_of by auto
with bound[unfolded deriv_bound_measure_class_def deriv_bound_rel_class_def
deriv_bound_rel_def] obtain n where "deriv_bound r t n" by blast
then have "SN_on r {t}"
by (rule deriv_bound_SN_on)
}
then show ?thesis unfolding SN_on_def by blast
qed
lemma deriv_bound_relto_measure_class_union:
assumes s1: "deriv_bound_measure_class (relto s1 (w ∪ s2)) as cc"
and s2: "deriv_bound_measure_class (relto s2 (w ∪ s1)) as cc"
shows "deriv_bound_measure_class (relto (s1 ∪ s2) w) as cc"
using s1 s2
unfolding deriv_bound_measure_class_def
by (rule deriv_bound_relto_class_union)
lemma deriv_bound_rel_mono:
assumes r: "r ⊆ r'⇧+" and as: "⋀ n. as n ⊆ as' n"
and f: "⋀ n. f' n ≤ f n"
and d: "deriv_bound_rel r' as' f'"
shows "deriv_bound_rel r as f" unfolding deriv_bound_rel_def
proof (intro allI impI)
fix n a
assume "a ∈ as n"
with as have "a ∈ as' n" by auto
from d [unfolded deriv_bound_rel_def, rule_format, OF this]
have "deriv_bound r' a (f' n)" .
from deriv_bound_mono [OF f this]
have "deriv_bound r' a (f n)" .
from deriv_bound_subset[OF r this]
show "deriv_bound r a (f n)" .
qed
lemma deriv_bound_rel_class_mono:
assumes r: "r ⊆ r'⇧+" and as: "⋀ n. as n ⊆ as' n"
and cc: "O_of cc' ⊆ O_of cc"
and d: "deriv_bound_rel_class r' as' cc'"
shows "deriv_bound_rel_class r as cc" unfolding deriv_bound_rel_class_def
proof -
from d obtain f where f: "f ∈ O_of cc'"
and d: "deriv_bound_rel r' as' f" by (auto simp: deriv_bound_rel_class_def)
from f and cc have "f ∈ O_of cc" by auto
with deriv_bound_rel_mono [OF r as le_refl d]
show "∃ f. f ∈ O_of cc ∧ deriv_bound_rel r as f" by auto
qed
lemma deriv_bound_measure_class_trancl_mono:
assumes r: "r ⊆ r'⇧+" and cm: "⋀ n. terms_of_nat cm n ⊆ terms_of_nat cm' n"
and cc: "O_of cc' ⊆ O_of cc"
and d: "deriv_bound_measure_class r' cm' cc'"
shows "deriv_bound_measure_class r cm cc" unfolding deriv_bound_measure_class_def
by (rule deriv_bound_rel_class_mono [OF r cm cc], rule d [unfolded deriv_bound_measure_class_def])
lemma deriv_bound_measure_class_mono:
assumes r: "r ⊆ r'" and cm: "⋀ n. terms_of_nat cm n ⊆ terms_of_nat cm' n"
and cc: "O_of cc' ⊆ O_of cc"
and d: "deriv_bound_measure_class r' cm' cc'"
shows "deriv_bound_measure_class r cm cc"
by (rule deriv_bound_measure_class_trancl_mono [OF _ cm cc d], insert r, auto)
lemma runtime_subset_derivational:
assumes F: "set C ∪ set D ⊆ set F"
shows "terms_of_nat (Runtime_Complexity C D) n ⊆ terms_of_nat (Derivational_Complexity F) n"
proof
fix t
assume t: "t ∈ terms_of_nat (Runtime_Complexity C D) n"
from t have n: "term_size t ≤ n" by simp
from t obtain f ts where f: "t = Fun f ts" by (cases t, auto)
from t f have D: "(f, length ts) ∈ set D" and C: "⋀ t. t ∈ set ts ⟹ funas_term t ⊆ set C"
by (auto simp: funas_args_term_def)
from D C F have "funas_term t ⊆ set F" unfolding f by auto
with t show "t ∈ terms_of_nat (Derivational_Complexity F) n" by simp
qed
fun get_signature_of_cm
where
"get_signature_of_cm (Derivational_Complexity F) = F" |
"get_signature_of_cm (Runtime_Complexity C D) = C @ D"
lemma get_signature_of_cm:
"terms_of_nat cm n ⊆ terms_of_nat (Derivational_Complexity (get_signature_of_cm cm)) n"
using runtime_subset_derivational [of _ _ _ n]
by (cases cm) (force simp: funas_args_term_def)+
end