theory ArityAnalysisSig
imports Terms AEnv "Arity-Nominal" "Nominal-HOLCF" "Substitution"
begin
locale ArityAnalysis =
fixes Aexp :: "exp \ Arity \ AEnv"
locale ArityAnalysisHeap =
fixes Aheap :: "heap \ exp \ Arity \ AEnv"
locale EdomArityAnalysis = ArityAnalysis +
assumes Aexp_edom: "edom (Aexp e\a) \ fv e"
begin
lemma fup_Aexp_edom: "edom (fup\(Aexp e)\a) \ fv e"
by (cases a) (auto dest:set_mp[OF Aexp_edom])
lemma Aexp_fresh_bot[simp]: assumes "atom v \ e" shows "(Aexp e\a) v = \"
proof-
from assms have "v \ fv e" by (metis fv_not_fresh)
with Aexp_edom have "v \ edom (Aexp e\a)" by auto
thus ?thesis unfolding edom_def by simp
qed
end
locale ArityAnalysisHeapEqvt = ArityAnalysisHeap +
assumes Aheap_eqvt[eqvt]: "\ \ Aheap = Aheap"
end