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

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

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