Theory ArityStack

theory ArityStack
imports Arity SestoftConf
begin

fun Astack :: "stack ⇒ Arity"
  where "Astack [] = 0"
      | "Astack (Arg x # S) = inc⋅(Astack S)"
      | "Astack (Alts e1 e2 # S) = 0"
      | "Astack (Upd x # S) = 0"
      | "Astack (Dummy x # S) = 0"

lemma Astack_restr_stack_below:
  "Astack (restr_stack V S) ⊑ Astack S"
  by (induction V S rule: restr_stack.induct) auto

lemma Astack_map_Dummy[simp]:
  "Astack (map Dummy l) = 0"
by (induction l) auto

lemma Astack_append_map_Dummy[simp]:
  "Astack S' = 0 ⟹ Astack (S @ S') = Astack S"
by (induction S rule: Astack.induct) auto


end