# Theory Derivation_Bound

theory Derivation_Bound
imports Abstract_Rewriting
```(*
Author:      René Thiemann
*)
section ‹Derivation Bounds›

text ‹Starting from this point onwards we apply the results on matrices to derive
complexity bounds in \isafor. So, here begins the connection to the definitions
and prerequisites that have originally been defined within \isafor.

This theory contains the notion of a derivation bound.›

theory Derivation_Bound
imports
"Abstract-Rewriting.Abstract_Rewriting"
begin

definition deriv_bound :: "'a rel ⇒ 'a ⇒ nat ⇒ bool"
where
"deriv_bound r a n ⟷ ¬ (∃ b. (a, b) ∈ r ^^ Suc n)"

lemma deriv_boundI [intro?]:
"(⋀b m. n < m ⟹ (a, b) ∈ r ^^ m ⟹ False) ⟹ deriv_bound r a n"
by (auto simp: deriv_bound_def) (metis lessI relpow_Suc_I)

lemma deriv_boundE:
assumes "deriv_bound r a n"
and "(⋀b m. n < m ⟹ (a, b) ∈ r ^^ m ⟹ False) ⟹ P"
shows "P"
using assms(1)
by (intro assms)

lemma deriv_bound_iff:
"deriv_bound r a n ⟷ (∀b m. n < m ⟶ (a, b) ∉ r ^^ m)"
by (auto elim: deriv_boundE intro: deriv_boundI)

lemma deriv_bound_empty [simp]:
"deriv_bound {} a n"

lemma deriv_bound_mono:
assumes "m ≤ n" and "deriv_bound r a m"
shows "deriv_bound r a n"
using assms by (auto simp: deriv_bound_iff)

lemma deriv_bound_image:
assumes b: "deriv_bound r' (f a) n"
and step: "⋀ a b. (a, b) ∈ r ⟹ (f a, f b) ∈ r'⇧+"
shows "deriv_bound r a n"
proof
fix b m
assume "(a, b) ∈ r ^^ m"
from relpow_image [OF step this] have "(f a, f b) ∈ r'⇧+ ^^ m" .
from trancl_steps_relpow [OF subset_refl this]
obtain k where "k ≥ m" and "(f a, f b) ∈ r' ^^ k" by auto
moreover assume "n < m"
moreover with deriv_bound_mono [OF _ b, of "m - 1"]
have "deriv_bound r' (f a) (m - 1)" by simp
ultimately show False using b by (simp add: deriv_bound_iff)
qed

lemma deriv_bound_subset:
assumes "r ⊆ r'⇧+"
and b: "deriv_bound r' a n"
shows "deriv_bound r a n"
using assms by (intro deriv_bound_image [of _ "λx. x", OF b]) auto

lemma deriv_bound_SN_on:
assumes "deriv_bound r a n"
shows "SN_on r {a}"
proof
fix f
assume steps: "∀ i. (f i, f (Suc i)) ∈ r" and "f 0 ∈ {a}"
with assms have "(f 0, f (Suc n)) ∉ r ^^ Suc n" by (blast elim: deriv_boundE)
moreover have "(f 0, f (Suc n)) ∈ r ^^ Suc n"
using steps unfolding relpow_fun_conv by (intro exI [of _ f]) auto
ultimately show False ..
qed

lemma deriv_bound_steps:
assumes "(a, b) ∈ r ^^ n"
and "deriv_bound r a m"
shows "n ≤ m"
using assms by (auto iff: not_less deriv_bound_iff)
end
```