theory ArityAnalysisSig imports "Terms" AEnv "Arity-Nominal" "Nominal-HOLCF" "Substitution" begin locale ArityAnalysis = fixes Aexp :: "exp ⇒ Arity → AEnv" begin abbreviation Aexp_syn ("𝒜⇘_⇙")where "𝒜⇘a⇙ e ≡ Aexp e⋅a" abbreviation Aexp_bot_syn ("𝒜⇧⊥⇘_⇙") where "𝒜⇧⊥⇘a⇙ e ≡ fup⋅(Aexp e)⋅a" end locale ArityAnalysisHeap = fixes Aheap :: "heap ⇒ exp ⇒ Arity → AEnv" locale EdomArityAnalysis = ArityAnalysis + assumes Aexp_edom: "edom (𝒜⇘a⇙ e) ⊆ fv e" begin lemma fup_Aexp_edom: "edom (𝒜⇧⊥⇘a⇙ e) ⊆ fv e" by (cases a) (auto dest:set_mp[OF Aexp_edom]) lemma Aexp_fresh_bot[simp]: assumes "atom v ♯ e" shows "𝒜⇘a⇙ e v = ⊥" proof- from assms have "v ∉ fv e" by (metis fv_not_fresh) with Aexp_edom have "v ∉ edom (𝒜⇘a⇙ e)" by auto thus ?thesis unfolding edom_def by simp qed end locale ArityAnalysisHeapEqvt = ArityAnalysisHeap + assumes Aheap_eqvt[eqvt]: "π ∙ Aheap = Aheap" end