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