Theory Derivation_Bound

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