Theory Status

section ‹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