Theory Derivation_Bound

theory Derivation_Bound
imports Abstract_Rewriting
    Author:      René Thiemann 
                 Akihisa Yamada
    License:     BSD
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

definition deriv_bound :: "'a rel ⇒ 'a ⇒ nat ⇒ bool"
  "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)
     (auto simp: deriv_bound_def relpow_add relcomp.simps dest!: less_imp_Suc_add, metis relpow_E2)

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"
  by (simp add: deriv_bound_def)

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"
  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)

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}"
  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 ..

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)