Theory ArityAnalysisStack

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!: subsetD[OF Aexp_edom])
end

end