Theory OpSem

(*  Title:      OpSem.thy
    Author:     Peter Gammie
*)

section ‹Logical relations for computational adequacy›
(*<*)

theory OpSem
imports
  Basis
  PCF
begin

(* FIXME

Show Sangiorgi's divergence results. Convergence should be simply the
big-step semantics.

*)
(*>*)
text‹

\label{sec:opsem}

We relate the denotational semantics for PCF of \S\ref{sec:densem} to
a \emph{big-step} (or \emph{natural}) operational semantics. This
follows citet‹"DBLP:conf/mfps/Pitts93"›.

›

subsection‹Direct semantics using de Bruijn notation›

text‹

\label{sec:directsem_db}

In contrast to \S\ref{sec:directsem} we must be more careful in our
treatment of ‹α›-equivalent terms, as we would like our
operational semantics to identify of all these. To that end we adopt
de Bruijn notation, adapting the work of
citet‹"DBLP:journals/jar/Nipkow01"›, and show that it is suitably
equivalent to our original syntactic story.

›

datatype db =
    DBVar var
  | DBApp db db
  | DBAbsN db
  | DBAbsV db
  | DBDiverge
  | DBFix db
  | DBtt
  | DBff
  | DBCond db db db
  | DBNum nat
  | DBSucc db
  | DBPred db
  | DBIsZero db

text‹

Nipkow et al's substitution operation is defined for arbitrary open
terms. In our case we only substitute closed terms into terms where
only the variable @{term "0"} may be free, and while we could develop
a simpler account, we retain the traditional one.

›

fun
  lift :: "db ⇒ nat ⇒ db"
where
  "lift (DBVar i) k = DBVar (if i < k then i else (i + 1))"
| "lift (DBAbsN s) k = DBAbsN (lift s (k + 1))"
| "lift (DBAbsV s) k = DBAbsV (lift s (k + 1))"
| "lift (DBApp s t) k = DBApp (lift s k) (lift t k)"
| "lift (DBFix e) k = DBFix (lift e (k + 1))"
| "lift (DBCond c t e) k = DBCond (lift c k) (lift t k) (lift e k)"
| "lift (DBSucc e) k = DBSucc (lift e k)"
| "lift (DBPred e) k = DBPred (lift e k)"
| "lift (DBIsZero e) k = DBIsZero (lift e k)"
| "lift x k = x"

fun
  subst :: "db ⇒ db ⇒ var ⇒ db"  ("_<_'/_>" [300, 0, 0] 300)
where
  subst_Var: "(DBVar i)<s/k> =
      (if k < i then DBVar (i - 1) else if i = k then s else DBVar i)"
| subst_AbsN: "(DBAbsN t)<s/k> = DBAbsN (t<lift s 0 / k+1>)"
| subst_AbsV: "(DBAbsV t)<s/k> = DBAbsV (t<lift s 0 / k+1>)"
| subst_App: "(DBApp t u)<s/k> = DBApp (t<s/k>) (u<s/k>)"
| "(DBFix e)<s/k> = DBFix (e<lift s 0 / k+1>)"
| "(DBCond c t e)<s/k> = DBCond (c<s/k>) (t<s/k>) (e<s/k>)"
| "(DBSucc e)<s/k> = DBSucc (e<s/k>)"
| "(DBPred e)<s/k> = DBPred (e<s/k>)"
| "(DBIsZero e)<s/k> = DBIsZero (e<s/k>)"
| subst_Consts: "x<s/k> = x"
(*<*)

declare subst_Var [simp del]

lemma subst_eq: "(DBVar k)<u/k> = u"
  by (simp add: subst_Var)

lemma subst_gt: "i < j ⟹ (DBVar j)<u/i> = DBVar (j - 1)"
  by (simp add: subst_Var)

lemma subst_lt: "j < i ⟹ (DBVar j)<u/i> = DBVar j"
  by (simp add: subst_Var)

lemma lift_lift:
    "i < k + 1 ⟹ lift (lift t i) (Suc k) = lift (lift t k) i"
  by (induct t arbitrary: i k) auto

lemma lift_subst:
    "j < i + 1 ⟹ lift (t<s/j>) i = (lift t (i + 1))<lift s i / j>"
  by (induct t arbitrary: i j s)
     (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)

lemma lift_subst_lt:
    "i < j + 1 ⟹ lift (t<s/j>) i = (lift t i)<lift s i / j + 1>"
  by (induct t arbitrary: i j s) (auto simp: subst_Var lift_lift)

lemma subst_lift:
    "(lift t k)<s/k> = t"
  by (induct t arbitrary: k s) (simp_all add: subst_eq subst_gt subst_lt)

lemmas subst_simps [simp] =
  subst_eq
  subst_gt
  subst_lt
  lift_subst
  subst_lift

lemma subst_subst:
    "i < j + 1 ⟹ t<lift v i/Suc j><u<v/j>/i> = t<u/i><v/j>"
  by (induct t arbitrary: i j u v)
     (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
             split: nat.split)

(*>*)
text‹

We elide the standard lemmas about these operations.

A variable is free in a de Bruijn term in the standard way.

›

fun
  freedb :: "db ⇒ var ⇒ bool"
where
  "freedb (DBVar j) k = (j = k)"
| "freedb (DBAbsN s) k = freedb s (k + 1)"
| "freedb (DBAbsV s) k = freedb s (k + 1)"
| "freedb (DBApp s t) k = (freedb s k ∨ freedb t k)"
| "freedb (DBFix e) k = freedb e (Suc k)"
| "freedb (DBCond c t e) k = (freedb c k ∨ freedb t k ∨ freedb e k)"
| "freedb (DBSucc e) k = freedb e k"
| "freedb (DBPred e) k = freedb e k "
| "freedb (DBIsZero e) k = freedb e k"
| "freedb _ _ = False"
(*<*)

lemma subst_not_free [simp]: "¬ freedb s i ⟹ s<t/i> = s<u/i>"
  by (induct s arbitrary: i t u) (simp_all add: subst_Var)

lemma free_lift [simp]:
  "freedb (lift t k) i ⟷ (i < k ∧ freedb t i ∨ k < i ∧ freedb t (i - 1))"
  by (induct t arbitrary: i k) (auto cong: conj_cong)

lemma free_subst [simp]:
  "freedb (s<t/k>) i ⟷ (freedb s k ∧ freedb t i ∨ freedb s (if i < k then i else i + 1))"
by (induct s arbitrary: i k t) (auto simp:  subst_Var split: nat.split)

theorem lift_subst_dummy:
  "¬ freedb s i ⟹ lift (s<dummy/i>) i = s"
by (induct s arbitrary: i dummy) (simp_all add: not_less_eq if_not_P)

lemma closed_lift:
  "∀v. freedb e v ⟶ v < k ⟹ lift e k = e"
by (induct e arbitrary: k) (simp; metis less_Suc_eq_0_disj nat.exhaust)+

lemma closed_subst:
  assumes "∀v. freedb e v ⟶ v < k"
  shows "e<s/k> = e"
using assms
proof(induct e arbitrary: s k)
  case (DBAbsN e) then show ?case by simp (metis lessE not_less_eq)
next
  case (DBAbsV e) then show ?case by simp (metis lessE not_less_eq)
next
  case (DBFix e) then show ?case by simp (metis lessE not_less_eq)
qed simp_all

(*>*)
text‹Programs are closed expressions.›

definition closed :: "db ⇒ bool" where
  "closed e ≡ ∀i. ¬ freedb e i"
(*<*)

lemma closed_inv:
  "closed (DBApp f x) ⟷ closed f ∧ closed x"
  "closed DBDiverge"
  "closed DBtt"
  "closed DBff"
  "closed (DBCond c t e) ⟷ closed c ∧ closed t ∧ closed e"
  "closed (DBNum n)"
  "closed (DBSucc e) ⟷ closed e"
  "closed (DBPred e) ⟷ closed e"
  "closed (DBIsZero e) ⟷ closed e"
  unfolding closed_def by auto

lemma closed_binders:
  "closed (DBAbsN e) ⟷ (∀i. freedb e i ⟶ i = 0)"
  "closed (DBAbsV e) ⟷ (∀i. freedb e i ⟶ i = 0)"
  "closed (DBFix e) ⟷ (∀i. freedb e i ⟶ i = 0)"
  unfolding closed_def
  apply auto
  apply (case_tac i, auto)+
  done

lemmas closed_invs [iff] =
  closed_inv
  closed_binders

(*>*)
text‹

The direct denotational semantics is almost identical to that given in
\S\ref{sec:densem}, apart from this change in the representation of
environments.

›

definition env_empty_db :: "'a Env" where
  "env_empty_db ≡ ⊥"

definition env_ext_db :: "'a → 'a Env → 'a Env" where
  "env_ext_db ≡ Λ x ρ v. (case v of 0 ⇒ x | Suc v' ⇒ ρ⋅v')"
(*<*)

lemma env_ext_same_db: "env_ext_db⋅x⋅ρ⋅0 = x"
  by (simp add: env_ext_db_def)

lemma env_ext_neq_db: "env_ext_db⋅x⋅ρ⋅(Suc v) = ρ⋅v"
  by (simp add: env_ext_db_def)

lemmas env_ext_db_simps [simp] =
  env_ext_same_db
  env_ext_neq_db
(*>*)
text‹›

primrec
  evalDdb :: "db ⇒ ValD Env → ValD"
where
  "evalDdb (DBVar i) = (Λ ρ. ρ⋅i)"
| "evalDdb (DBApp f x) = (Λ ρ. appF⋅(evalDdb f⋅ρ)⋅(evalDdb x⋅ρ))"
| "evalDdb (DBAbsN e) = (Λ ρ. ValF⋅(Λ x. evalDdb e⋅(env_ext_db⋅x⋅ρ)))"
| "evalDdb (DBAbsV e) = (Λ ρ. ValF⋅(strictify⋅(Λ x. evalDdb e⋅(env_ext_db⋅x⋅ρ))))"
| "evalDdb (DBDiverge) = (Λ ρ. ⊥)"
| "evalDdb (DBFix e) = (Λ ρ. μ x. evalDdb e⋅(env_ext_db⋅x⋅ρ))"
| "evalDdb (DBtt) = (Λ ρ. ValTT)"
| "evalDdb (DBff) = (Λ ρ. ValFF)"
| "evalDdb (DBCond c t e) = (Λ ρ. cond⋅(evalDdb c⋅ρ)⋅(evalDdb t⋅ρ)⋅(evalDdb e⋅ρ))"
| "evalDdb (DBNum n) = (Λ ρ. ValN⋅n)"
| "evalDdb (DBSucc e) = (Λ ρ. succ⋅(evalDdb e⋅ρ))"
| "evalDdb (DBPred e) = (Λ ρ. pred⋅(evalDdb e⋅ρ))"
| "evalDdb (DBIsZero e) = (Λ ρ. isZero⋅(evalDdb e⋅ρ))"
(*<*)

(* This proof is trivial but Isabelle doesn't seem keen enough to
apply the induction hypothesises in the obvious ways. *)
lemma evalDdb_env_cong:
  assumes "∀v. freedb e v ⟶ ρ⋅v = ρ'⋅v"
  shows "evalDdb e⋅ρ = evalDdb e⋅ρ'"
using assms
proof(induct e arbitrary: ρ ρ')
  case (DBApp e1 e2 ρ ρ')
  from DBApp.hyps[where ρ=ρ and ρ'=ρ'] DBApp.prems show ?case by simp
next
  case (DBAbsN e ρ ρ')
  { fix x
    from DBAbsN.hyps[where ρ="env_ext_db⋅x⋅ρ" and ρ'="env_ext_db⋅x⋅ρ'"] DBAbsN.prems
    have "evalDdb e⋅(env_ext_db⋅x⋅ρ) = evalDdb e⋅(env_ext_db⋅x⋅ρ')"
      by (simp add: env_ext_db_def split: nat.splits) }
  then show ?case by simp
next
  case (DBAbsV e ρ ρ')
  { fix x
    from DBAbsV.hyps[where ρ="env_ext_db⋅x⋅ρ" and ρ'="env_ext_db⋅x⋅ρ'"] DBAbsV.prems
    have "evalDdb e⋅(env_ext_db⋅x⋅ρ) = evalDdb e⋅(env_ext_db⋅x⋅ρ')"
      by (simp add: env_ext_db_def split: nat.splits) }
  then show ?case by simp
next
  case (DBFix e ρ ρ') then show ?case
    by simp (rule parallel_fix_ind, simp_all add: env_ext_db_def split: nat.splits)
next
  case (DBCond i t e ρ ρ')
  from DBCond.hyps[where ρ=ρ and ρ'=ρ'] DBCond.prems show ?case by simp
next
  case (DBSucc e ρ ρ')
  from DBSucc.hyps[where ρ=ρ and ρ'=ρ'] DBSucc.prems show ?case by simp
next
  case (DBPred e ρ ρ')
  from DBPred.hyps[where ρ=ρ and ρ'=ρ'] DBPred.prems show ?case by simp
next
  case (DBIsZero e ρ ρ')
  from DBIsZero.hyps[where ρ=ρ and ρ'=ρ'] DBIsZero.prems show ?case by simp
qed (auto simp: cfun_eq_iff)

lemma evalDdb_env_closed:
  assumes "closed e"
  shows "evalDdb e⋅ρ = evalDdb e⋅ρ'"
by (rule evalDdb_env_cong) (simp add: assms[unfolded closed_def])

(*>*)
text‹

We show that our direct semantics using de Bruijn notation coincides
with the evaluator of \S\ref{sec:directsem} by translating between the
syntaxes and showing that the evaluators yield identical results.

Firstly we show how to translate an expression using names into a
nameless term. The following function finds the first mention of a
variable in a list of variables.

›

primrec index :: "var list ⇒ var ⇒ nat ⇒ nat" where
  "index [] v n = n"
| "index (h # t) v n = (if v = h then n else index t v (Suc n))"

primrec
  transdb :: "expr ⇒ var list ⇒ db"
where
  "transdb (Var i) Γ = DBVar (index Γ i 0)"
| "transdb (App t1 t2) Γ = DBApp (transdb t1 Γ) (transdb t2 Γ)"
| "transdb (AbsN v t) Γ = DBAbsN (transdb t (v # Γ))"
| "transdb (AbsV v t) Γ = DBAbsV (transdb t (v # Γ))"
| "transdb (Diverge) Γ = DBDiverge"
| "transdb (Fix v e) Γ = DBFix (transdb e (v # Γ))"
| "transdb (tt) Γ = DBtt"
| "transdb (ff) Γ = DBff"
| "transdb (Cond c t e) Γ = DBCond (transdb c Γ) (transdb t Γ) (transdb e Γ)"
| "transdb (Num n) Γ = (DBNum n)"
| "transdb (Succ e) Γ = DBSucc (transdb e Γ)"
| "transdb (Pred e) Γ = DBPred (transdb e Γ)"
| "transdb (IsZero e) Γ = DBIsZero (transdb e Γ)"

text‹

This semantics corresponds with the direct semantics for named
expressions.

›
(*<*)
text‹The free variables of an expression using names.›

fun
  free :: "expr ⇒ var list"
where
  "free (Var v) = [v]"
| "free (App f x) = free f @ free x"
| "free (AbsN v e) = removeAll v (free e)"
| "free (AbsV v e) = removeAll v (free e)"
| "free (Fix v e) = removeAll v (free e)"
| "free (Cond c t e) = free c @ free t @ free e"
| "free (Succ e) = free e"
| "free (Pred e) = free e"
| "free (IsZero e) = free e"
| "free _ = []"

lemma index_Suc:
  "index Γ v (Suc i) = Suc (index Γ v i)"
  by (induct Γ arbitrary: i) simp_all

lemma evalD_evalDdb_open:
  assumes "set (free e) ⊆ set Γ"
  assumes "∀v ∈ set Γ. ρ'⋅(index Γ v 0) = ρ⋅v"
  shows "⟦e⟧ρ = evalDdb (transdb e Γ)⋅ρ'"
using assms
proof(induct e arbitrary: Γ ρ ρ')
  case AbsN then show ?case
    apply (clarsimp simp: cfun_eq_iff)
    apply (subst AbsN.hyps)
    apply (auto simp: cfun_eq_iff env_ext_db_def index_Suc)
    done
next
  case AbsV then show ?case
    apply (clarsimp simp: cfun_eq_iff)
    apply (case_tac "x=⊥")
     apply simp
    apply simp
    apply (subst AbsV.hyps)
    apply (auto simp: cfun_eq_iff env_ext_db_def index_Suc)
    done
next
  case Fix then show ?case
    apply (clarsimp simp: cfun_eq_iff)
    apply (rule parallel_fix_ind)
      apply simp
     apply simp
    apply simp
    apply (subst Fix.hyps)
    apply (auto simp: cfun_eq_iff env_ext_db_def index_Suc)
    done
qed auto

(*>*)
lemma evalD_evalDdb:
  assumes "free e = []"
  shows "⟦e⟧ρ = evalDdb (transdb e [])⋅ρ"
  using assms by (simp add: evalD_evalDdb_open)

text‹

Conversely, all de Bruijn expressions have named equivalents.

›

primrec
  transdb_inv :: "db ⇒ (var ⇒ var) ⇒ var ⇒ var ⇒ expr"
where
  "transdb_inv (DBVar i) Γ c k = Var (Γ i)"
| "transdb_inv (DBApp t1 t2) Γ c k = App (transdb_inv t1 Γ c k) (transdb_inv t2 Γ c k)"
| "transdb_inv (DBAbsN e) Γ c k = AbsN (c + k) (transdb_inv e (case_nat (c + k) Γ) c (k + 1))"
| "transdb_inv (DBAbsV e) Γ c k = AbsV (c + k) (transdb_inv e (case_nat (c + k) Γ) c (k + 1))"
| "transdb_inv (DBDiverge) Γ c k = Diverge"
| "transdb_inv (DBFix e) Γ c k = Fix (c + k) (transdb_inv e (case_nat (c + k) Γ) c (k + 1))"
| "transdb_inv (DBtt) Γ c k = tt"
| "transdb_inv (DBff) Γ c k = ff"
| "transdb_inv (DBCond i t e) Γ c k =
                     Cond (transdb_inv i Γ c k) (transdb_inv t Γ c k) (transdb_inv e Γ c k)"
| "transdb_inv (DBNum n) Γ c k = (Num n)"
| "transdb_inv (DBSucc e) Γ c k = Succ (transdb_inv e Γ c k)"
| "transdb_inv (DBPred e) Γ c k = Pred (transdb_inv e Γ c k)"
| "transdb_inv (DBIsZero e) Γ c k = IsZero (transdb_inv e Γ c k)"
(*<*)

(* FIXME These proofs are ghastly. Is there a better way to do this? *)

lemma transdb_inv_open:
  assumes "∀v. freedb e v ⟶ v < c + k"
  assumes "∀v. freedb e v ⟶ Γ v = (if k ≤ v then v - k else c + k - v - 1)"
  assumes "∀v. freedb e v ⟶ (if k ≤ v then index Γ' (v - k) 0 = v else index Γ' (c + k - v - 1) 0 = v)"
  shows "transdb (transdb_inv e Γ c k) Γ' = e"
using assms
proof(induct e arbitrary: Γ Γ' k)
  case DBVar then show ?case by (simp split: if_splits)
next
  case (DBApp e1 e2 Γ Γ') then show ?case
    apply -
    apply (drule_tac x=k in meta_spec)+
    apply (drule_tac x=Γ in meta_spec, drule_tac x=Γ' in meta_spec)+
    apply auto
    done
next
  case (DBAbsN e Γ Γ' k) show ?case
    apply simp
    apply (rule DBAbsN.hyps)

    using DBAbsN
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp

    using DBAbsN
    apply (clarsimp split: nat.split)

    using DBAbsN
    apply clarsimp
    apply (case_tac v)
    apply (auto simp: index_Suc)
    done
next
  case (DBAbsV e Γ Γ' k) show ?case
    apply simp
    apply (rule DBAbsV.hyps)

    using DBAbsV
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp

    using DBAbsV
    apply (clarsimp split: nat.split)

    using DBAbsV
    apply clarsimp
    apply (case_tac v)
    apply (auto simp: index_Suc)
    done
next
  case (DBFix e Γ Γ' k) show ?case
    apply simp
    apply (rule DBFix.hyps)

    using DBFix
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp

    using DBFix
    apply (clarsimp split: nat.split)

    using DBFix
    apply clarsimp
    apply (case_tac v)
    apply (auto simp: index_Suc)
    done
next
  case (DBCond i t e Γ Γ' k) then show ?case
    apply -
    apply (drule_tac x=k in meta_spec)+
    apply (drule_tac x=Γ in meta_spec, drule_tac x=Γ' in meta_spec)+
    apply auto
    done
qed simp_all

(*>*)
text‹›

lemma transdb_inv:
  assumes "closed e"
  shows "transdb (transdb_inv e Γ c k) Γ' = e"
(*<*)
  using transdb_inv_open assms
  unfolding closed_def by simp

lemma closed_transdb_inv_aux:
  assumes "∀v. freedb e v ⟶ v < k"
  assumes "∀v. freedb e v ⟶ Γ v = k - v - 1"
  shows "i ∈ set (free (transdb_inv e Γ 0 k)) ⟷ (i < k ∧ freedb e (k - i - 1))"
using assms
proof(induct e arbitrary: Γ k)
  case (DBAbsN e Γ k) then show ?case
    apply -
    apply (drule_tac x="Suc k" in meta_spec)
    apply (drule_tac x="case_nat k Γ" in meta_spec)
    apply simp
    apply (subgoal_tac "∀v. freedb e v ⟶ v < Suc k")
     apply (subgoal_tac "∀v. freedb e v ⟶ case_nat k Γ v = k - v")
      apply rule
       apply (subgoal_tac "Suc (k - Suc i) = k - i")
        apply simp
       apply auto[1]
      apply (subgoal_tac "Suc (k - Suc i) = k - i")
       apply auto[1]
      apply auto[1]
     apply (auto split: nat.splits)[1]
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp
    done
next
  case (DBAbsV e Γ k) then show ?case
    apply -
    apply (drule_tac x="Suc k" in meta_spec)
    apply (drule_tac x="case_nat k Γ" in meta_spec)
    apply simp
    apply (subgoal_tac "∀v. freedb e v ⟶ v < Suc k")
     apply (subgoal_tac "∀v. freedb e v ⟶ case_nat k Γ v = k - v")
      apply rule
       apply (subgoal_tac "Suc (k - Suc i) = k - i")
        apply simp
       apply auto[1]
      apply (subgoal_tac "Suc (k - Suc i) = k - i")
       apply auto[1]
      apply auto[1]
     apply (auto split: nat.splits)[1]
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp
    done
next
  case (DBFix e Γ k) then show ?case
    apply -
    apply (drule_tac x="Suc k" in meta_spec)
    apply (drule_tac x="case_nat k Γ" in meta_spec)
    apply simp
    apply (subgoal_tac "∀v. freedb e v ⟶ v < Suc k")
     apply (subgoal_tac "∀v. freedb e v ⟶ case_nat k Γ v = k - v")
      apply rule
       apply (subgoal_tac "Suc (k - Suc i) = k - i")
        apply simp
       apply auto[1]
      apply (subgoal_tac "Suc (k - Suc i) = k - i")
       apply auto[1]
      apply auto[1]
     apply (auto split: nat.splits)[1]
    apply clarsimp
    apply (case_tac v)
     apply simp
    apply simp
    done
qed auto

lemma closed_transdb_inv:
  assumes "closed e"
  shows "free (transdb_inv e Γ 0 0) = []"
  using assms closed_transdb_inv_aux[where e=e and k=0 and Γ=Γ]
  unfolding closed_def by fastforce

(*>*)


subsection‹Operational Semantics›

text ‹

The evaluation relation (big-step, or natural operational
semantics). This is similar to citet‹‹\S6.2› in "Gunter:1992"›,
citet‹"DBLP:conf/mfps/Pitts93"› and citet‹‹Chapter~11› in "Winskel:1993"›.

We firstly define the \emph{values} that expressions can evaluate to:
these are either constants or closed abstractions.

›

inductive
  val :: "db ⇒ bool"
where
  v_Num[intro]: "val (DBNum n)"
| v_FF[intro]:  "val DBff"
| v_TT[intro]:  "val DBtt"
| v_AbsN[intro]: "val (DBAbsN e)"
| v_AbsV[intro]: "val (DBAbsV e)"

inductive
  evalOP :: "db ⇒ db ⇒ bool" ("_ ⇓ _" [50,50] 50)
where
  evalOP_AppN[intro]:  "⟦ P ⇓ DBAbsN M; M<Q/0> ⇓ V ⟧ ⟹ DBApp P Q ⇓ V" (* Non-strict application *)
| evalOP_AppV[intro]:  "⟦ P ⇓ DBAbsV M; Q ⇓ q; M<q/0> ⇓ V ⟧ ⟹ DBApp P Q ⇓ V" (* Strict application *)
| evalOP_AbsN[intro]:  "val (DBAbsN e) ⟹ DBAbsN e ⇓ DBAbsN e"
| evalOP_AbsV[intro]:  "val (DBAbsV e) ⟹ DBAbsV e ⇓ DBAbsV e"
| evalOP_Fix[intro]: "P<DBFix P/0> ⇓ V ⟹ DBFix P ⇓ V" (* Non-strict fix *)
| evalOP_tt[intro]:  "DBtt ⇓ DBtt"
| evalOP_ff[intro]:  "DBff ⇓ DBff"
| evalOP_CondTT[intro]: "⟦ C ⇓ DBtt; T ⇓ V ⟧ ⟹ DBCond C T E ⇓ V"
| evalOP_CondFF[intro]: "⟦ C ⇓ DBff; E ⇓ V ⟧ ⟹ DBCond C T E  ⇓ V"
| evalOP_Num[intro]:  "DBNum n ⇓ DBNum n"
| evalOP_Succ[intro]: "P ⇓ DBNum n ⟹ DBSucc P ⇓ DBNum (Suc n)"
| evalOP_Pred[intro]: "P ⇓ DBNum (Suc n) ⟹ DBPred P ⇓ DBNum n"
| evalOP_IsZeroTT[intro]: "⟦ E ⇓ DBNum 0 ⟧ ⟹ DBIsZero E ⇓ DBtt"
| evalOP_IsZeroFF[intro]: "⟦ E ⇓ DBNum n; 0 < n ⟧ ⟹ DBIsZero E ⇓ DBff"

text‹

It is straightforward to show that this relation is deterministic and
sound with respect to the denotational semantics.

›
(*<*)

inductive_cases evalOP_inv [elim]:
  "DBApp P Q ⇓ v"
  "DBAbsN e ⇓ v"
  "DBAbsV e ⇓ v"
  "DBFix P ⇓ v"
  "DBtt ⇓ v"
  "DBff ⇓ v"
  "DBCond C T E ⇓ v"
  "DBNum n ⇓ v"
  "DBSucc E ⇓ v"
  "DBPred E ⇓ v"
  "DBIsZero E ⇓ v"

lemma eval_val:
  assumes "val t"
  shows "t ⇓ t"
using assms by induct blast+

lemma eval_to [iff]:
  assumes "t ⇓ t'"
  shows "val t'"
using assms by induct blast+

lemma evalOP_deterministic:
  assumes "P ⇓ V"
  assumes "P ⇓ V'"
  shows "V = V'"
using assms
proof(induct arbitrary: V' rule: evalOP.induct)
  case evalOP_AppV then show ?case by (metis db.distinct(47) db.inject(4) evalOP_inv(1))
qed blast+

lemma evalOP_closed:
  assumes "P ⇓ V"
  assumes "closed P"
  shows "closed V"
using assms
apply induct
apply auto
using closed_def apply force+
done

text‹The denotational semantics respects substitution.›

lemma evalDdb_lift [simp]:
  "evalDdb (lift s k)⋅ρ = evalDdb s⋅(Λ i. if i < k then ρ⋅i else ρ⋅(Suc i))"
proof(induct s arbitrary: k ρ)
  case DBAbsN then show ?case
    apply (clarsimp simp: cfun_eq_iff env_ext_db_def)
    apply (rule cfun_arg_cong)
    apply (auto split: nat.split simp: cfun_eq_iff)
    done
next
  case DBAbsV then show ?case
    apply (clarsimp simp: cfun_eq_iff env_ext_db_def)
    apply (case_tac "x=⊥")
     apply simp
    apply (intro cfun_cong)
    apply (auto split: nat.split simp: cfun_eq_iff cong: cfun_cong)
    apply (intro cfun_cong) (* FIXME weird *)
    apply (auto split: nat.split simp: cfun_eq_iff cong: cfun_cong)
    done
next
  case (DBFix s k ρ) then show ?case
    apply (clarsimp simp: cfun_eq_iff env_ext_db_def)
    apply (rule parallel_fix_ind)
      apply simp
     apply simp
    apply simp
    apply (rule cfun_arg_cong)
    apply (auto split: nat.split simp: cfun_eq_iff)
    done
qed simp_all

lemma evalDdb_subst:
  "evalDdb (e<s/x>)⋅ρ = evalDdb e⋅(Λ i. if x < i then ρ⋅(i - 1) else if i = x then evalDdb s⋅ρ else ρ⋅i)"
proof(induct e arbitrary: s x ρ)
  case (DBFix e s x ρ) then show ?case
    apply (simp only: evalDdb.simps subst.simps)
    apply (rule parallel_fix_ind)
    apply (auto simp: cfun_eq_iff eta_cfun env_ext_db_def split: nat.split intro!: cfun_cong)
    done
qed (auto simp: cfun_eq_iff eta_cfun env_ext_db_def split: nat.split intro!: cfun_cong)

lemma evalDdb_subst_env_ext_db:
  "evalDdb (e<s/0>)⋅ρ = evalDdb e⋅(env_ext_db⋅(evalDdb s⋅ρ)⋅ρ)"
by (auto simp: evalDdb_subst env_ext_db_def cfun_eq_iff split: nat.split intro!: cfun_arg_cong)

lemma eval_val_not_bot:
  assumes "P ⇓ V"
  shows "evalDdb V⋅ρ ≠ ⊥"
by (rule val.induct[OF eval_to[OF assms]], simp_all)

(*>*)
theorem evalOP_sound:
  assumes "P ⇓ V"
  shows "evalDdb P⋅ρ = evalDdb V⋅ρ"
(*<*)
using assms
proof(induct arbitrary: ρ)
  case evalOP_AppN then show ?case
    by (simp add: evalOP_AppN(4)[symmetric] evalDdb_subst_env_ext_db)
next
  case (evalOP_AppV P M Q q V ρ) then show ?case
    apply simp
    apply (subst evalOP_AppV(4)[symmetric])
    apply (simp add: eval_val_not_bot strictify_cancel evalDdb_subst_env_ext_db)
    done
next
  case (evalOP_Fix P V ρ)
  have "evalDdb V⋅ρ = evalDdb (P<DBFix P/0>)⋅ρ"
    using evalOP_Fix by simp
  also have "... = evalDdb P⋅(Λ i. if 0 < i then ρ⋅(i - 1) else if i = 0 then (μ x. evalDdb P⋅(env_ext_db⋅x⋅ρ)) else ρ⋅i)"
    apply (simp add: evalDdb_subst)
    apply (rule cfun_arg_cong)
    apply (simp add: cfun_eq_iff)
    done
  also have "... = evalDdb (DBFix P)⋅ρ"
    apply simp
    apply (subst (2) fix_eq)
    apply (simp add: env_ext_db_def)
    apply (rule cfun_arg_cong)
    apply (auto simp: cfun_eq_iff env_ext_db_def split: nat.split)
    done
  finally show ?case by simp
qed (simp_all add: cond_def isZero_def pred_def succ_def)

(*>*)
text‹

We can use soundness to conclude that POR is not definable
operationally either. We rely on @{thm [source] "transdb_inv"} to map
our de Bruijn term into the syntactic universe of
\S\ref{sec:directsem} and appeal to the results of
\S\ref{sec:por}. This takes some effort as @{typ "ValD"} contains
irrelevant junk that makes it hard to draw obvious conclusions; we use
‹DBCond› to restrict the arguments to the putative witness.

›

definition
  "isPORdb e ≡ closed e
    ∧ DBApp (DBApp e DBtt) DBDiverge ⇓ DBtt
    ∧ DBApp (DBApp e DBDiverge) DBtt ⇓ DBtt
    ∧ DBApp (DBApp e DBff) DBff ⇓ DBff"

(*<*)
lemma ValD_strict:
  "⟦ f⋅a⋅b = ValTT; f⋅x⋅y = ValFF ⟧ ⟹ f⋅⊥⋅⊥ = ⊥"
using monofun_cfun[OF monofun_cfun_arg[where f=f and x="⊥" and y=x], where x="⊥" and y=y, simplified]
      monofun_cfun[OF monofun_cfun_arg[where f=f and x="⊥" and y=a], where x="⊥" and y=b, simplified]
by (cases "f⋅⊥⋅⊥") simp_all

lemma ValD_ValTT:
  "⟦ f⋅⊥⋅ValTT = ValTT; f⋅ValTT⋅⊥ = ValTT ⟧ ⟹ f⋅ValTT⋅ValTT = ValTT"
using monofun_cfun[OF monofun_cfun_arg[where f=f and x="⊥"], where x="ValTT" and y="ValTT"]
by (cases "f⋅ValTT⋅ValTT") simp_all
(*>*)

lemma POR_is_not_operationally_definable: "¬isPORdb e"
(*<*)
proof(rule notI)
  assume P: "isPORdb e"
  let ?porV = "ValF⋅(Λ x. ValF⋅(Λ y. x por y))"
  from P have "closed e
     ∧ evalDdb (DBApp (DBApp e DBtt) DBDiverge)⋅ρ = ValTT
     ∧ evalDdb (DBApp (DBApp e DBDiverge) DBtt)⋅ρ = ValTT
     ∧ evalDdb (DBApp (DBApp e DBff) DBff)⋅ρ = ValFF" for ρ
    unfolding isPORdb_def by (force dest!: evalOP_sound[where ρ=ρ])
  then have F: "closed e
      ∧ ⟦transdb_inv (DBApp (DBApp e DBtt) DBDiverge) id 0 0⟧ρ = ValTT
      ∧ ⟦transdb_inv (DBApp (DBApp e DBDiverge) DBtt) id 0 0⟧ρ = ValTT
      ∧ ⟦transdb_inv (DBApp (DBApp e DBff) DBff) id 0 0⟧ρ = ValFF" for ρ
    (* id is arbitrary here *)
    by (simp add: evalD_evalDdb transdb_inv closed_transdb_inv)
  from F have G: "appF⋅(appF⋅(⟦transdb_inv e id 0 0⟧ρ)⋅⊥)⋅⊥ = ⊥" for ρ
    by (auto intro: ValD_strict[where f="Λ x y. appF⋅(appF⋅(⟦transdb_inv e id 0 0⟧ρ)⋅x)⋅y", simplified])
  from F have H: "appF⋅(appF⋅(⟦transdb_inv e id 0 0⟧ρ)⋅ValTT)⋅ValTT = ValTT" for ρ
    using ValD_ValTT[where f="Λ x y. appF⋅(appF⋅(⟦transdb_inv e id 0 0⟧ρ)⋅x)⋅y"] by simp
  let ?f = "AbsN 0 (AbsN 1 (App (App (transdb_inv e id 0 0)
                                     (Cond (Var 0) (Var 0) (Cond (Var 1) (Var 1) (Var 1))) )
                                     (Cond (Var 1) (Var 1) (Cond (Var 0) (Var 0) (Var 0))) ))"
  from F G H have "⟦?f⟧env_empty = ?porV"
    apply (clarsimp simp: cfun_eq_iff cond_def)
    apply (case_tac x, simp_all)
     apply (case_tac xa, simp_all)+
    done
  with POR_sat have "definable ?porV ∧ appFLv ?porV [POR_arg1_rel, POR_arg2_rel] = POR_result_rel"
    unfolding definable_def by blast
  with POR_is_not_definable show False by blast
qed
(*>*)


subsection‹Computational Adequacy›

text‹

\label{sec:compad}

The lemma @{thm [source] "evalOP_sound"} tells us that the operational
semantics preserves the denotational semantics. We might also hope
that the two are somehow equivalent, but due to the junk in the
domain-theoretic model (see \S\ref{sec:pcfdefinability}) we cannot
expect this to be entirely straightforward. Here we show that the
denotational semantics is \emph{computationally adequate}, which means
that it can be used to soundly reason about contextual equivalence.

We follow citet‹"DBLP:conf/mfps/Pitts93" and "PittsAM:relpod"› by defining a
suitable logical relation between our @{typ "ValD"} domain and the set
of programs (closed terms). These are termed "formal approximation
relations" by Plotkin. The machinery of \S\ref{sec:synlr} requires us
to define a unique bottom element, which in this case is @{term "{⊥} ×
{ P . closed P}"}. To that end we define the type of programs.

›

typedef Prog = "{ P. closed P }"
  morphisms unProg mkProg by fastforce

definition
  ca_lf_rep :: "(ValD, Prog) synlf_rep"
where
  "ca_lf_rep ≡ λ(rm, rp).
     ({⊥} × UNIV)
     ∪ { (d, P) |d P.
        (∃n. d = ValN⋅n ∧ unProg P ⇓ DBNum n)
      ∨ (d = ValTT ∧ unProg P ⇓ DBtt)
      ∨ (d = ValFF ∧ unProg P ⇓ DBff)
      ∨ (∃f M. d = ValF⋅f ∧ unProg P ⇓ DBAbsN M
              ∧ (∀(x, X) ∈ unsynlr (undual rm). (f⋅x, mkProg (M<unProg X/0>)) ∈ unsynlr rp))
      ∨ (∃f M. d = ValF⋅f ∧ unProg P ⇓ DBAbsV M ∧ f⋅⊥ = ⊥
              ∧ (∀(x, X) ∈ unsynlr (undual rm). ∀V. unProg X ⇓ V
                     ⟶ (f⋅x, mkProg (M<V/0>)) ∈ unsynlr rp)) }"

abbreviation ca_lr :: "(ValD, Prog) synlf" where
  "ca_lr ≡ λr. mksynlr (ca_lf_rep r)"

text‹

Intuitively we relate domain-theoretic values to all programs that
converge to the corresponding syntatic values. If a program has a
non-@{term "⊥"} denotation then we can use this relation to conclude
something about the value it (operationally) converges to.

›
(*<*)

lemmas Prog_simps [iff] =
  unProg_inverse
  mkProg_inverse[simplified]

lemma bot_ca_lf_rep [intro, simp]:
  "(⊥, P) ∈ ca_lf_rep r"
  unfolding ca_lf_rep_def by (simp add: split_def)

lemma synlr_cal_lr_rep [intro, simp]:
  "ca_lf_rep r ∈ synlr"
  unfolding ca_lf_rep_def
  by rule (auto intro!: adm_conj adm_disj adm_below_monic_exists
                  simp: split_def
                  dest: evalOP_deterministic)

lemma mono_ca_lr:
  "mono ca_lr"
proof
  fix x y :: "(ValD, Prog) synlr dual × (ValD, Prog) synlr"
  obtain x1 x2 y1 y2 where [simp]: "x = (x1, x2)" "y = (y1, y2)"
    by (cases x, cases y)
  assume "x ≤ y"
  then have "ca_lf_rep (x1, x2) ⊆ ca_lf_rep (y1, y2)"
    by (simp add: ca_lf_rep_def unsynlr_leq [symmetric] dual_less_eq_iff split_def)
      fastforce
  then show "ca_lr x ≤ ca_lr y"
    by simp
qed

lemma min_inv_ca_lr:
  assumes "e⋅⊥ = ⊥"
  assumes "eRSS e R' S'"
  shows "eRSS (ValD_copy_rec⋅e) (dual (ca_lr (dual S', undual R'))) (ca_lr (R', S'))"
  apply simp
  unfolding ca_lf_rep_def using assms
  apply simp
  apply (rule ballI)
  apply (simp add: split_def)
  apply (elim disjE)
  apply fastforce
  apply fastforce
  apply fastforce
  apply fastforce

  (* FIXME fastforce gets lost ?? AbsN *)
  apply clarsimp
  apply (rule_tac x=M in exI)
  apply clarsimp
  apply (frule (1) bspec)
  apply simp
  apply (frule (1) bspec) back
  apply simp
  apply (frule (1) bspec) back
  apply simp

  (* FIXME fastforce gets lost ?? AbsV *)
  apply (intro disjI2)
  apply clarsimp
  apply (rule_tac x=M in exI)
  apply clarsimp
  apply (frule (1) bspec)
  apply simp
  apply (frule (1) bspec) back
  apply simp
  apply (frule (1) bspec) back
  apply bestsimp
  done

(*>*)
text‹›

interpretation ca: DomSolSyn ca_lr ValD_copy_rec
  apply standard
     apply (rule mono_ca_lr)
    apply (rule ValD_copy_ID)
   apply simp
  apply (erule (1) min_inv_ca_lr)
  done

definition ca_lr_syn :: "ValD ⇒ db ⇒ bool" ("_ ◃ _" [80,80] 80) where
  "d ◃ P ≡ (d, P) ∈ { (x, unProg Y) |x Y. (x, Y) ∈ unsynlr ca.delta }"
(*<*)

lemma adm_ca_lr [intro, simp]:
  "closed P ⟹ adm (λx. x ◃ P)"
  unfolding ca_lr_syn_def
  by (auto simp: unProg_inject)

lemma closed_ca_lr [intro]:
  "d ◃ P ⟹ closed P"
  apply (subst (asm) ca_lr_syn_def)
  apply (subst (asm) ca.delta_sol)
  apply simp
  apply (clarsimp simp: ca_lf_rep_def)
  apply (case_tac Y)
  apply simp
  done

lemma ca_lrI [intro, simp]:
  "closed P ⟹ ⊥ ◃ P"
  "⟦ P ⇓ DBtt; closed P ⟧ ⟹ ValTT ◃ P"
  "⟦ P ⇓ DBff; closed P ⟧ ⟹ ValFF ◃ P"
  "⟦ P ⇓ DBNum n; closed P ⟧ ⟹ ValN⋅n ◃ P"
  apply (simp_all add: ca_lr_syn_def)
  apply (simp add: exI[where x="mkProg P"])
  apply ((subst ca.delta_sol, simp, subst ca_lf_rep_def, simp add: exI[where x="mkProg P"])+)
  done

lemma ca_lr_DBAbsNI:
  "⟦ P ⇓ DBAbsN M; closed P; ⋀x X. x ◃ X ⟹ f⋅x ◃ M<X/0> ⟧ ⟹ ValF⋅f ◃ P"
  apply (simp add: ca_lr_syn_def)
  apply (subst ca.delta_sol)
  apply simp
  apply (rule exI[where x="mkProg P"])
  apply (subst ca_lf_rep_def)
  apply simp
  apply (rule disjI1)
  apply (rule exI[where x=M])
  apply force
  done

lemma ca_lr_DBAbsVI:
  "⟦ P ⇓ DBAbsV M; closed P; f⋅⊥ = ⊥; ⋀x X V. ⟦ x ◃ X; X ⇓ V ⟧ ⟹ f⋅x ◃ M<V/0> ⟧ ⟹ ValF⋅f ◃ P"
  apply (simp add: ca_lr_syn_def)
  apply (subst ca.delta_sol)
  apply simp
  apply (rule exI[where x="mkProg P"])
  apply (subst ca_lf_rep_def)
  apply simp
  apply force
  done

lemma ca_lrE:
  "⟦ d ◃ P;
     ⟦ d = ⊥; closed P ⟧ ⟹ Q;
     ⟦ d = ValTT; closed P; P ⇓ DBtt ⟧ ⟹ Q;
     ⟦ d = ValFF; closed P; P ⇓ DBff ⟧ ⟹ Q;
     ⋀n. ⟦ d = ValN⋅n; closed P; P ⇓ DBNum n ⟧ ⟹ Q;
     ⋀f M. ⟦ d = ValF⋅f; closed P; P ⇓ DBAbsN M; ⋀x X. x ◃ X ⟹ f⋅x ◃ M<X/0> ⟧ ⟹ Q;
     ⋀f M. ⟦ d = ValF⋅f; f⋅⊥ = ⊥; closed P; P ⇓ DBAbsV M; ⋀x X V. ⟦ x ◃ X; X ⇓ V ⟧ ⟹ f⋅x ◃ M<V/0> ⟧ ⟹ Q
   ⟧ ⟹ Q"
  apply (frule closed_ca_lr)
  apply (simp add: ca_lr_syn_def)
  apply (subst (asm) ca.delta_sol)
  apply simp
  apply (subst (asm) ca_lf_rep_def)
  apply clarsimp
  apply (case_tac Y)
  apply (elim disjE)
  apply auto

  apply (drule_tac x=f in meta_spec)
  apply (drule_tac x=M in meta_spec)
  apply simp
  apply (subgoal_tac "(⋀x X. ∃Y. X = unProg Y ∧ (x, Y) ∈ unsynlr (DomSolSyn.delta ca_lr) ⟹ ∃Y. M<X/0> = unProg Y ∧ (f⋅x, Y) ∈ unsynlr (DomSolSyn.delta ca_lr))")
   apply blast
  apply clarsimp
  apply (rule_tac x="mkProg (M<unProg Y/0>)" in exI)
  apply auto[1]
  apply (subst mkProg_inverse)
   apply simp
  apply (frule (1) evalOP_closed)
  apply (subst (asm) closed_binders)
  apply (auto simp: closed_def
             split: nat.splits)[2]
  apply (case_tac Y)
  apply (auto simp: closed_def)[1]

  apply (drule_tac x=f in meta_spec) back
  apply (drule_tac x=M in meta_spec)
  apply simp
  apply (subgoal_tac "(⋀x X V. ⟦∃Y. X = unProg Y ∧ (x, Y) ∈ unsynlr (DomSolSyn.delta ca_lr); X ⇓ V⟧
                      ⟹ ∃Y. M<V/0> = unProg Y ∧ (f⋅x, Y) ∈ unsynlr (DomSolSyn.delta ca_lr))")
   apply blast
  apply clarsimp
  apply (drule (1) bspec)
  apply clarsimp
  apply (rule_tac x="mkProg (M<V/0>)" in exI)
  apply clarsimp
  apply (subst mkProg_inverse)
   defer
   apply simp
  apply simp
  apply (drule (1) evalOP_closed)
  using closed_def closed_invs(11) evalOP_closed unProg by force

(*>*)
text‹

To establish this result we need a ``closing substitution'' operation.
It seems easier to define it directly in this simple-minded way than
reusing the standard substitution operation.

This is quite similar to a context-plugging (non-capturing)
substitution operation, where the ``holes'' are free variables, and
indeed we use it as such below.

›

fun
  closing_subst :: "db ⇒ (var ⇒ db) ⇒ var ⇒ db"
where
  "closing_subst (DBVar i) Γ k = (if k ≤ i then Γ (i - k) else DBVar i)"
| "closing_subst (DBApp t u) Γ k = DBApp (closing_subst t Γ k) (closing_subst u Γ k)"
| "closing_subst (DBAbsN t) Γ k = DBAbsN (closing_subst t Γ (k + 1))"
| "closing_subst (DBAbsV t) Γ k = DBAbsV (closing_subst t Γ (k + 1))"
| "closing_subst (DBFix e) Γ k = DBFix (closing_subst e Γ (k + 1))"
| "closing_subst (DBCond c t e) Γ k =
            DBCond (closing_subst c Γ k) (closing_subst t Γ k) (closing_subst e Γ k)"
| "closing_subst (DBSucc e) Γ k = DBSucc (closing_subst e Γ k)"
| "closing_subst (DBPred e) Γ k = DBPred (closing_subst e Γ k)"
| "closing_subst (DBIsZero e) Γ k = DBIsZero (closing_subst e Γ k)"
| "closing_subst x Γ k = x"

text‹

We can show it has the expected properties when all terms in @{term
"Γ"} are closed.

›

(*<*)
lemma freedb_closing_subst [iff]:
  assumes "∀v. freedb e v ∧ k ≤ v ⟶ closed (Γ (v - k))"
  shows "freedb (closing_subst e Γ k) i ⟷ (freedb e i ∧ i < k)"
  using assms
  apply (induct e arbitrary: i k)
  using Suc_le_D
  apply (auto simp: closed_def not_less_eq diff_Suc split: nat.split)
    apply (subgoal_tac "∀v. freedb e v ∧ Suc k ≤ v ⟶ (∀j. ¬ freedb (Γ (v - Suc k)) j)"; use Suc_le_D in force)+
    done

lemma closed_closing_subst [intro, simp]:
  assumes "∀v. freedb e v ⟶ closed (Γ v)"
  shows "closed (closing_subst e Γ 0)"
using assms freedb_closing_subst[where e=e and k=0]
unfolding closed_def by fastforce

lemma subst_closing_subst:
  assumes "∀v. freedb e v ∧ k < v ⟶ closed (Γ (v - Suc k))"
  assumes "closed X"
  shows "(closing_subst e Γ (Suc k))<X/k> = closing_subst e (case_nat X Γ) k"
using assms
proof(induct e arbitrary: k)
  case DBVar then show ?case
    unfolding closed_def
    by (clarsimp simp: Suc_le_eq closed_subst) (metis Suc_diff_Suc old.nat.simps(5))
next
  case DBAbsN then show ?case
    by clarsimp (metis Suc_less_eq2 closed_def closed_lift diff_Suc_Suc)
next
  case DBAbsV then show ?case
    by clarsimp (metis Suc_less_eq2 closed_def closed_lift diff_Suc_Suc)
next
  case DBFix then show ?case
    by clarsimp (metis Suc_less_eq2 closed_def closed_lift diff_Suc_Suc)
qed (auto simp: not_less_eq split: nat.split)

lemma closing_subst_closed [intro, simp]:
  assumes "∀v. freedb e v ⟶ v < k"
  shows "closing_subst e Γ k = e"
  using assms
  apply (induct e arbitrary: k)
  apply (auto simp: closed_def)
  apply (metis gr_implies_not0 nat.exhaust not_less_eq)+
  done

lemma closing_subst_evalDdb_cong:
  assumes "∀v. closed (Γ v) ∧ closed (Γ' v)"
  assumes "∀v. evalDdb (Γ v)⋅env_empty_db = evalDdb (Γ' v)⋅env_empty_db"
  shows "evalDdb (closing_subst e Γ k)⋅ρ = evalDdb (closing_subst e Γ' k)⋅ρ"
proof(induct e arbitrary: k ρ)
  case DBVar with assms show ?case
    by (simp; subst (1 2) evalDdb_env_closed[where ρ'=env_empty_db]; simp)
qed auto

(*>*)
text‹

The key lemma is shown by induction over @{term "e"} for arbitrary
environments (@{term "Γ"} and @{term "ρ"}):

›

lemma ca_open:
  assumes "∀v. freedb e v ⟶ ρ⋅v ◃ Γ v ∧ closed (Γ v)"
  shows "evalDdb e⋅ρ ◃ closing_subst e Γ 0"
(*<*)
using assms
proof(induct e arbitrary: Γ ρ)
  case (DBApp e1 e2 Γ ρ)
  from DBApp.prems DBApp.hyps[of ρ Γ] show ?case
    apply simp
    apply (erule ca_lrE)
     apply simp_all

    apply (drule_tac x="evalDdb e2⋅ρ" in meta_spec)
    apply (drule_tac x="closing_subst e2 Γ 0" in meta_spec)
    apply simp
    apply (erule ca_lrE) back
     apply (auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI)[6]

    apply (case_tac "evalDdb e2⋅ρ = ⊥")
     apply simp
    apply (subgoal_tac "∃V. closing_subst e2 Γ 0 ⇓ V")
     apply clarsimp
     apply (drule_tac x="evalDdb e2⋅ρ" in meta_spec)
      apply (drule_tac x="closing_subst e2 Γ 0" in meta_spec)
      apply (drule_tac x="V" in meta_spec)
      apply simp
      apply (erule ca_lrE) back
       apply (auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI)[6]
    apply (erule ca_lrE)
    apply auto
    done
next
  case (DBAbsN e Γ ρ)
  from DBAbsN.prems show ?case
    apply simp
    apply (rule ca_lr_DBAbsNI)
      apply (rule eval_val)
      apply (rule v_AbsN)
      apply (clarsimp simp: closed_def split: nat.split)
     apply clarsimp
    apply (subst subst_closing_subst)
      apply simp
     apply blast
    apply (cut_tac ρ="env_ext_db⋅x⋅ρ" and Γ="case_nat X Γ" in DBAbsN.hyps)
     apply (subgoal_tac "∀v. freedb e v ⟶ env_ext_db⋅x⋅ρ⋅v ◃ case_nat X Γ v ∧ closed (case_nat X Γ v)")
      apply blast
     apply (auto simp: env_ext_db_def split: nat.splits)
    done
next
  case (DBAbsV e Γ ρ)
  from DBAbsV.prems show ?case
    apply simp
    apply (rule ca_lr_DBAbsVI)
       apply (rule eval_val)
       apply (rule v_AbsV)
      apply (clarsimp simp: closed_def split: nat.split)
     apply clarsimp
    apply (frule closed_ca_lr)
    apply (frule (1) evalOP_closed)
    apply (case_tac "x=⊥")
     apply simp
      apply (rule ca_lrI)
     apply (subst subst_closing_subst)
       apply simp
      apply simp
     apply (simp add: nat.split_sels(1))
    apply simp
    apply (subst subst_closing_subst)
      apply simp
     apply blast
    apply (cut_tac ρ="env_ext_db⋅x⋅ρ" and Γ="case_nat V Γ" in DBAbsV.hyps)
     apply (subgoal_tac "∀v. freedb e v ⟶ env_ext_db⋅x⋅ρ⋅v ◃ case_nat V Γ v ∧ closed (case_nat V Γ v)")
      apply blast
     apply (auto simp: env_ext_db_def split: nat.splits)
    apply (erule ca_lrE)
         apply ((blast dest: evalOP_deterministic)+)[4]
     apply clarsimp
     apply (subgoal_tac "V = DBAbsN M")
      apply clarsimp
      apply (rule ca_lr_DBAbsNI)
      apply (rule eval_val)
      apply (auto dest: evalOP_deterministic)[4]
    apply (subgoal_tac "V = DBAbsV M")
     apply clarsimp
     apply (rule ca_lr_DBAbsVI)
     apply (auto dest: evalOP_deterministic)
    done
next
  case (DBFix e Γ ρ) then show ?case
    apply simp
    apply (rule fix_ind)
      apply simp_all
    apply (drule_tac x="env_ext_db⋅x⋅ρ" in meta_spec)
    apply (drule_tac x="case_nat (closing_subst (DBFix e) Γ 0) Γ" in meta_spec)
    apply (subgoal_tac "∀v. freedb e v ⟶ env_ext_db⋅x⋅ρ⋅v ◃ case_nat (closing_subst (DBFix e) Γ 0) Γ v ∧ closed (case_nat (closing_subst (DBFix e) Γ 0) Γ v)")
     apply clarsimp
     apply (erule ca_lrE) back
      apply auto[1]

      apply simp
      apply (rule ca_lrI)
       apply (auto simp: subst_closing_subst)[2]

      apply simp
      apply (rule ca_lrI)
       apply (auto simp: subst_closing_subst)[2]

      apply simp
      apply (rule ca_lrI)
       apply (auto simp: subst_closing_subst)[2]

      apply simp
      apply (rule ca_lr_DBAbsNI)
       apply (auto simp: subst_closing_subst)[3]

      apply simp
      apply (rule ca_lr_DBAbsVI)
       apply (auto simp: subst_closing_subst)[3]
       apply force

      apply (clarsimp simp: env_ext_db_def split: nat.split)
    done
next
  case (DBCond c t e Γ ρ) then show ?case
    apply (simp add: cond_def)
    apply (drule_tac x=ρ in meta_spec, drule_tac x=Γ in meta_spec)+
    apply simp
    apply (erule ca_lrE, auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI)+
    done
next
  case (DBSucc e Γ ρ) then show ?case
    apply (simp add: succ_def)
    apply (drule_tac x=ρ in meta_spec, drule_tac x=Γ in meta_spec)
    apply simp
    apply (erule ca_lrE, auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI)+
    done
next
  case (DBPred e Γ ρ) then show ?case
    apply (simp add: pred_def)
    apply (drule_tac x=ρ in meta_spec, drule_tac x=Γ in meta_spec)
    apply simp
    apply (erule ca_lrE, auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI split: nat.split)+
    done
next
  case (DBIsZero e Γ ρ) then show ?case
    apply (simp add: isZero_def)
    apply (drule_tac x=ρ in meta_spec, drule_tac x=Γ in meta_spec)
    apply simp
    apply (erule ca_lrE, auto intro: ca_lr_DBAbsNI ca_lr_DBAbsVI)+
    done
qed auto

(*>*)
text‹›

lemma ca_closed:
  assumes "closed e"
  shows "evalDdb e⋅env_empty_db ◃ e"
  using ca_open[where e=e and ρ=env_empty_db] assms
  by (simp add: closed_def)

theorem ca:
  assumes nb: "evalDdb e⋅env_empty_db ≠ ⊥"
  assumes "closed e"
  shows "∃V. e ⇓ V"
  using ca_closed[OF ‹closed e›] nb
  by (auto elim!: ca_lrE)

text‹

This last result justifies reasoning about contextual equivalence
using the denotational semantics, as we now show.

›


subsubsection‹Contextual Equivalence›

text‹

As we are using an un(i)typed language, we take a context @{term "C"}
to be an arbitrary term, where the free variables are the
``holes''. We substitute a closed expression @{term "e"} uniformly for
all of the free variables in @{term "C"}. If open, the term @{term
"e"} can be closed using enough @{term "AbsN"}s. This seems to be a
standard trick now, see e.g. citet‹"DBLP:conf/popl/KoutavasW06"›. If we
didn't have CBN (only CBV) then it might be worth showing that this is
an adequate treatment.

›

definition ctxt_sub :: "db ⇒ db ⇒ db" ("(_<_>)" [300, 0] 300) where
  "C<e> ≡ closing_subst C (λ_. e) 0"
(*<*)

lemma ctxt_sub_closed [iff]:
  "closed e ⟹ closed (C<e>)"
  unfolding ctxt_sub_def by simp

lemma ctxt_sub_cong:
  assumes "closed e1"
  assumes "closed e2"
  assumes "evalDdb e1⋅env_empty_db = evalDdb e2⋅env_empty_db"
  shows "evalDdb (C<e1>)⋅env_empty_db = evalDdb (C<e2>)⋅env_empty_db"
  unfolding ctxt_sub_def using assms by (auto intro: closing_subst_evalDdb_cong)

(*>*)
text‹

Following citet‹"PittsAM:relpod"› we define a relation between values
that ``have the same form''. This is weak at functional values. We
don't distinguish between strict and non-strict abstractions.

›

inductive
  have_the_same_form :: "db ⇒ db ⇒ bool" ("_ ∼ _" [50,50] 50)
where
  "DBAbsN e ∼ DBAbsN e'"
| "DBAbsN e ∼ DBAbsV e'"
| "DBAbsV e ∼ DBAbsN e'"
| "DBAbsV e ∼ DBAbsV e'"
| "DBFix e ∼ DBFix e'"
| "DBtt ∼ DBtt"
| "DBff ∼ DBff"
| "DBNum n ∼ DBNum n"
(*<*)

declare have_the_same_form.intros [intro, simp]

lemma have_the_same_form_sound:
  assumes D: "evalDdb v1⋅ρ = evalDdb v2⋅ρ"
  assumes "val v1"
  assumes "val v2"
  shows "v1 ∼ v2"
  using ‹val v1› D
  apply (induct rule: val.induct)
  apply simp_all
  using ‹val v2›
  apply (induct rule: val.induct)
  apply simp_all
  using ‹val v2›
  apply (induct rule: val.induct)
  apply simp_all
  using ‹val v2›
  apply (induct rule: val.induct)
  apply simp_all
  using ‹val v2›
  apply (induct rule: val.induct)
  apply simp_all
  using ‹val v2›
  apply (induct rule: val.induct)
  apply simp_all
  done

(* FIXME could also show compatability, i.e. that the
contextually_equivalent relation is compatible with the language. *)

(*>*)
text‹

A program @{term "e2"} \emph{refines} the program @{term "e1"} if it
converges in context at least as often. This is a preorder on
programs.

›

definition
  refines :: "db ⇒ db ⇒ bool" ("_ ⊴ _" [50,50] 50)
where
  "e1 ⊴ e2 ≡ ∀C. ∃V1. C<e1> ⇓ V1 ⟶ (∃V2. C<e2> ⇓ V2 ∧ V1 ∼ V2)"

text‹

Contextually-equivalent programs refine each other.

›

definition
  contextually_equivalent :: "db ⇒ db ⇒ bool" ("_ ≈ _")
where
  "e1 ≈ e2 ≡ e1 ⊴ e2 ∧ e2 ⊴ e1"
(*<*)

lemma refinesI:
  "(⋀C V1. C<e1> ⇓ V1 ⟹ (∃V2. C<e2> ⇓ V2 ∧ V1 ∼ V2))
     ⟹ e1 ⊴ e2"
  unfolding refines_def by blast

lemma computational_adequacy_refines:
  assumes "closed e1"
  assumes "closed e2"
  assumes e: "evalDdb e1⋅env_empty_db = evalDdb e2⋅env_empty_db"
  shows "e1 ⊴ e2"
proof(rule refinesI)
  fix C V1 assume V1: "C<e1> ⇓ V1"
  from assms have D: "evalDdb (C<e2>)⋅env_empty_db = evalDdb (C<e1>)⋅env_empty_db"
    by (metis ctxt_sub_cong)
  from D ‹closed e2› obtain V2 where V2: "C<e2> ⇓ V2"
    using evalOP_sound[OF V1] ca[where e="C<e2>"] eval_val_not_bot[OF V1]
    by auto
  from D V1 V2 have V1V2: "evalDdb V1⋅env_empty_db = evalDdb V2⋅env_empty_db"
    by (simp add: evalOP_sound)
  from V1 V2 V1V2
  show "∃V2. C<e2> ⇓ V2 ∧ V1 ∼ V2"
    by (auto simp: have_the_same_form_sound)
qed

(*>*)
text‹

Our ultimate theorem states that if two programs have the same
denotation then they are contextually equivalent.

›

theorem computational_adequacy:
  assumes 1: "closed e1"
  assumes 2: "closed e2"
  assumes D: "evalDdb e1⋅env_empty_db = evalDdb e2⋅env_empty_db"
  shows "e1 ≈ e2"
(*<*)
  using assms
  unfolding contextually_equivalent_def
  by (simp add: computational_adequacy_refines)
(*>*)

text‹

This gives us a sound but incomplete method for demonstrating
contextual equivalence. We expect this result is useful for showing
contextual equivalence for \emph{typed} programs as well, but leave it
to future work to demonstrate this.

See citet‹‹\S6.2› in "Gunter:1992"› for further discussion of computational
adequacy at higher types.

The reader may wonder why we did not use Nominal syntax to define our
operational semantics, following
citet‹"DBLP:journals/entcs/UrbanN09"›. The reason is that Nominal2 does
not support the definition of continuous functions over Nominal
syntax, which is required by the evaluators of \S\ref{sec:directsem}
and \S\ref{sec:directsem_db}. As observed above, in the setting of
traditional programming language semantics one can get by with a much
simpler notion of substitution than is needed for investigations into
‹λ›-calculi. Clearly this does not hold of languages that
reduce ``under binders''.

The ``fast and loose reasoning is morally correct'' work of
citet‹"DBLP:conf/popl/DanielssonHJG06"› can be seen as a kind of
adequacy result.

citet‹"DBLP:conf/tphol/BentonKV09"› demonstrate a similar computational
adequacy result in Coq. However their system is only geared up for
this kind of metatheory, and not reasoning about particular programs;
its term language is combinatory.

citet‹"DBLP:conf/ppdp/BentonKBH07" and "DBLP:conf/ppdp/BentonKBH09"› have
shown that it is difficult to scale this domain-theoretic approach up
to richer languages, such as those with dynamic allocation of mutable
references, especially if these references can contain (arbitrary)
functional values.

›

(*<*)

end
(*>*)