Theory ArityAnalysisSig

theory ArityAnalysisSig
imports Launchbury.Terms AEnv "Arity-Nominal" "Launchbury.Nominal-HOLCF"  Launchbury.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:subsetD[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