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