theory ArityAnalysisStack
imports "SestoftConf" "ArityAnalysisSig"
begin
context ArityAnalysis
begin
fun AEstack :: "Arity list \ stack \ AEnv"
where
"AEstack _ [] = \"
| "AEstack (a#as) (Alts e1 e2 # S) = Aexp e1\a \ Aexp e2\a \ AEstack as S"
| "AEstack as (Upd x # S) = esing x\(up\0) \ AEstack as S"
| "AEstack as (Arg x # S) = esing x\(up\0) \ AEstack as S"
| "AEstack as (_ # S) = AEstack as S"
end
context EdomArityAnalysis
begin
lemma edom_AEstack: "edom (AEstack as S) \ fv S"
by (induction as S rule: AEstack.induct) (auto simp del: fun_meet_simp dest!: set_mp[OF Aexp_edom])
end
end