Theory HasESem

theory HasESem
imports "Nominal-HOLCF" "Env-HOLCF"
begin

text {*
A local to work abstract in the expression type and semantics.
*}

locale has_ESem =
  fixes ESem :: "'exp::pt ⇒ ('var::at_base ⇒ 'value) → 'value::{pure,pcpo}" 
begin
  abbreviation ESem_syn ("⟦ _ ⟧⇘_⇙"  [0,0] 110) where "⟦e⟧⇘ρ⇙ ≡ ESem e ⋅ ρ"
end

locale has_ignore_fresh_ESem = has_ESem +
  assumes fv_supp: "supp e = atom ` (fv e :: 'b set)"
  assumes ESem_considers_fv: "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f|` (fv e)⇙"

end