# Theory Status

section ‹Preliminaries›
subsection ‹Status functions›
text ‹A status function assigns to each n-ary symbol a list of indices between 0 and n-1.
These functions are encapsulated into a separate type, so that recursion on the i-th subterm
does not have to perform out-of-bounds checks (e.g., to ensure termination).›
theory Status
imports
First_Order_Terms.Term
begin
typedef 'f status = "{ (σ :: 'f × nat ⇒ nat list). (∀ f k. set (σ (f, k)) ⊆ {0 ..< k})}"
morphisms status Abs_status
by (rule exI[of _ "λ _. []"]) auto
setup_lifting type_definition_status
lemma status: "set (status σ (f, n)) ⊆ {0 ..< n}"
by (transfer) auto
lemma status_aux[termination_simp]: "i ∈ set (status σ (f, length ss)) ⟹ ss ! i ∈ set ss"
using status[of σ f "length ss"] unfolding set_conv_nth by force
lemma status_termination_simps[termination_simp]:
assumes i1: "i < length (status σ (f, length xs))"
shows "size (xs ! (status σ (f, length xs) ! i)) < Suc (size_list size xs)" (is "?a < ?c")
proof -
from i1 have "status σ (f, length xs) ! i ∈ set (status σ (f, length xs))" by auto
from status_aux[OF this] have "?a ≤ size_list size xs" by (auto simp: termination_simp)
then show ?thesis by auto
qed
lemma status_ne:
"status σ (f, n) ≠ [] ⟹ ∃i < n. i ∈ set (status σ (f, n))"
using status [of σ f n]
by (meson atLeastLessThan_iff set_empty subsetCE subsetI subset_empty)
lemma set_status_nth:
"length xs = n ⟹ i ∈ set (status σ (f, n)) ⟹ i < length xs ∧ xs ! i ∈ set xs"
using status [of σ f n] by force
lift_definition full_status :: "'f status" is "λ (f, n). [0 ..< n]" by auto
lemma full_status[simp]: "status full_status (f, n) = [0 ..< n]"
by transfer auto
text ‹An argument position i is simple wrt. some term relation, if the i-th subterm is in relation to the
full term.›
definition simple_arg_pos :: "('f, 'v) term rel ⇒ 'f × nat ⇒ nat ⇒ bool" where
"simple_arg_pos rel f i ≡ ∀ ts. i < snd f ⟶ length ts = snd f ⟶ (Fun (fst f) ts, ts ! i) ∈ rel"
lemma simple_arg_posI: "⟦⋀ ts. length ts = n ⟹ i < n ⟹ (Fun f ts, ts ! i) ∈ rel⟧ ⟹ simple_arg_pos rel (f, n) i"
unfolding simple_arg_pos_def by auto
end