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