Theory Abstract-Denotational-Props

theory "Abstract-Denotational-Props"
  imports AbstractDenotational Substitution
begin

context semantic_domain
begin

subsubsection ‹The semantics ignores fresh variables›

lemma ESem_considers_fv': "⟦ e ⟧⇘ρ⇙ = ⟦ e ⟧⇘ρ f|` (fv e)⇙"
proof (induct e arbitrary: ρ rule:exp_induct)
  case Var
  show ?case by simp
next
  have [simp]: "⋀ S x. S ∩ insert x S = S" by auto
  case App
  show ?case
    by (simp, subst (1 2) App, simp)
next
  case (Lam x e)
  show ?case by simp
next
  case (IfThenElse scrut e⇩1 e⇩2)
  have [simp]: "(fv scrut ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv scrut" by auto
  have [simp]: "(fv e⇩1 ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv e⇩1" by auto
  have [simp]: "(fv e⇩2 ∩ (fv scrut ∪ fv e⇩1 ∪ fv e⇩2)) = fv e⇩2" by auto
  show ?case
    apply simp
    apply (subst (1 2) IfThenElse(1))
    apply (subst (1 2) IfThenElse(2))
    apply (subst (1 2) IfThenElse(3))
    apply (simp)
    done
next
  case (Let as e)

  have "⟦e⟧⇘⦃as⦄ρ⇙ = ⟦e⟧⇘(⦃as⦄ρ) f|` (fv as ∪ fv e)⇙"
    apply (subst (1 2) Let(2))
    apply simp
    done
  also
  have "fv as ⊆ fv as ∪ fv e" by (rule inf_sup_ord(3))
  hence "(⦃as⦄ρ) f|` (fv as ∪ fv e) = ⦃as⦄(ρ f|` (fv as ∪ fv e))"
     by (rule HSem_ignores_fresh_restr'[OF _ Let(1)])
  also
  have "⦃as⦄(ρ f|` (fv as ∪ fv e)) = ⦃as⦄ρ f|` (fv as ∪ fv e - domA as)"
    by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq)
  finally
  show ?case by simp
qed auto

sublocale has_ignore_fresh_ESem ESem
  by standard (rule fv_supp_exp, rule ESem_considers_fv')

subsubsection ‹Nicer equations for ESem, without freshness requirements›

lemma ESem_Lam[simp]: "⟦ Lam [x]. e ⟧⇘ρ⇙ = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v)⇙))"
proof-
  have *: "⋀ v. ((ρ f|` (fv e - {x}))(x := v)) f|` fv e = (ρ(x := v)) f|` fv e"
    by (rule ext) (auto simp add: lookup_env_restr_eq)

  have "⟦ Lam [x]. e ⟧⇘ρ⇙ = ⟦ Lam [x]. e ⟧⇘env_delete x ρ⇙"
    by (rule ESem_fresh_cong) simp
  also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘(ρ f|` (fv e - {x}))(x := v)⇙))"
    by simp
  also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘((ρ f|` (fv e - {x}))(x := v)) f|` fv e⇙))"
    by (subst  ESem_considers_fv, rule)
  also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v) f|` fv e⇙))"
    unfolding *..
  also have "… = tick ⋅ (Fn ⋅ (Λ v. ⟦ e ⟧⇘ρ(x := v)⇙))"
    unfolding  ESem_considers_fv[symmetric]..
  finally show ?thesis.
qed
declare ESem.simps(1)[simp del]

lemma ESem_Let[simp]: "⟦Let as body⟧⇘ρ⇙ = tick ⋅ (⟦body⟧⇘⦃as⦄ρ⇙)"
proof-
  have "⟦ Let as body ⟧⇘ρ⇙ = tick ⋅ (⟦body⟧⇘⦃as⦄(ρ f|` fv (Let as body))⇙)" 
    by simp
  also have "⦃as⦄(ρ f|` fv(Let as body)) = ⦃as⦄(ρ f|` (fv as ∪ fv body))" 
    by (rule HSem_restr_cong) (auto simp add: lookup_env_restr_eq)
  also have "… = (⦃as⦄ρ) f|` (fv as ∪ fv body)"
    by (rule HSem_ignores_fresh_restr'[symmetric, OF _ ESem_considers_fv]) simp
  also have "⟦body⟧⇘…⇙ = ⟦body⟧⇘⦃as⦄ρ⇙"
    by (rule ESem_fresh_cong) (auto simp add: lookup_env_restr_eq)
  finally show ?thesis.
qed
declare ESem.simps(4)[simp del]


subsubsection ‹Denotation of Substitution›

lemma ESem_subst_same: "ρ x = ρ y ⟹  ⟦ e ⟧⇘ρ⇙ = ⟦ e[x::= y] ⟧⇘ρ⇙"
  and 
  "ρ x = ρ y  ⟹  (❙⟦ as ❙⟧⇘ρ⇙) = ❙⟦ as[x::h=y] ❙⟧⇘ρ⇙"
proof (nominal_induct e and as avoiding: x y arbitrary: ρ and ρ rule:exp_heap_strong_induct)
case Var thus ?case by auto
next
case App
  from App(1)[OF App(2)] App(2)
  show ?case by auto
next
case (Let as exp x y ρ)
  from ‹atom ` domA as ♯* x› ‹atom ` domA as  ♯* y› 
  have "x ∉ domA as" "y ∉ domA as"
    by (metis fresh_star_at_base imageI)+
  hence [simp]:"domA (as[x::h=y]) = domA as" 
    by (metis bn_subst)

  from ‹ρ x = ρ y›
  have "(⦃as⦄ρ) x = (⦃as⦄ρ) y"
    using ‹x ∉ domA as› ‹y ∉ domA as›
    by (simp add: lookup_HSem_other)
  hence "⟦exp⟧⇘⦃as⦄ρ⇙ = ⟦exp[x::=y]⟧⇘⦃as⦄ρ⇙"
    by (rule Let)
  moreover
  from ‹ρ x = ρ y›
  have "⦃as⦄ρ = ⦃as[x::h=y]⦄ρ" and "(⦃as⦄ρ) x = (⦃as[x::h=y]⦄ρ) y"
    apply (induction rule: parallel_HSem_ind)
    apply (intro adm_lemmas cont2cont cont2cont_fun)
    apply simp
    apply simp
    apply simp
    apply (erule arg_cong[OF Let(3)])
    using ‹x ∉ domA as› ‹y ∉ domA as›
    apply simp
    done
  ultimately
  show ?case using Let(1,2,3) by (simp add: fresh_star_Pair)
next
case (Lam var exp x y ρ)
  from ‹ρ x = ρ y›
  have "⋀v. (ρ(var := v)) x = (ρ(var := v)) y"
    using Lam(1,2) by (simp add: fresh_at_base)
  hence "⋀ v. ⟦exp⟧⇘ρ(var := v)⇙ = ⟦exp[x::=y]⟧⇘ρ(var := v)⇙"
    by (rule Lam)
  thus ?case using Lam(1,2) by simp
next
case IfThenElse
  from IfThenElse(1)[OF IfThenElse(4)] IfThenElse(2)[OF IfThenElse(4)] IfThenElse(3)[OF IfThenElse(4)]
  show ?case
    by simp
next
case Nil thus ?case by auto
next
case Cons
  from Cons(1,2)[OF Cons(3)] Cons(3)
  show ?case by auto
qed auto

lemma ESem_subst:
  shows "⟦ e ⟧⇘σ(x := σ y)⇙ = ⟦ e[x::= y] ⟧⇘σ⇙"
proof(cases "x = y")
  case False
  hence [simp]: "x ∉ fv e[x::=y]" by (auto simp add: fv_def supp_subst supp_at_base dest: subsetD[OF supp_subst]) 

  have "⟦ e ⟧⇘σ(x := σ y)⇙ = ⟦ e[x::= y] ⟧⇘σ(x := σ y)⇙"
    by (rule ESem_subst_same) simp
  also have "… = ⟦ e[x::= y] ⟧⇘σ⇙"
    by (rule ESem_fresh_cong) simp
  finally
  show ?thesis.
next
  case True
  thus ?thesis by simp
qed

end

end