Theory Continuations

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

section ‹Relating direct and continuation semantics›
(*<*)
theory Continuations
imports
  PCF
begin

(*>*)
text‹

\label{sec:continuations}

This is a fairly literal version of
citet"DBLP:conf/icalp/Reynolds74", adapted to untyped PCF. A more
abstract account has been given by
citet"DBLP:journals/tcs/Filinski07" in terms of a monadic meta
language, which is difficult to model in Isabelle (but see
citet"Huffman:MonadTransformers:2012").

We begin by giving PCF a continuation semantics following the modern
account of citet"wadler92:_essence_of_funct_progr".  We use the
symmetric function space ('o ValK, 'o) K → ('o ValK, 'o) K›
as our language includes call-by-name.

›

type_synonym ('a, 'o) K = "('a  'o)  'o"

domain 'o ValK
  = ValKF (lazy appKF :: "('o ValK, 'o) K  ('o ValK, 'o) K")
  | ValKTT | ValKFF
  | ValKN (lazy "nat")

type_synonym 'o ValKM = "('o ValK, 'o) K"
(*<*)

lemma ValK_case_ID [simp]:
  "ValK_caseValKFValKTTValKFFValKN = ID"
  apply (rule cfun_eqI)
  apply (case_tac x)
  apply simp_all
  done

lemma below_monic_ValKF [iff]:
  "below_monic_cfun ValKF"
  by (rule below_monicI) simp

lemma below_monic_ValKN [iff]:
  "below_monic_cfun ValKN"
  by (rule below_monicI) simp

(*>*)
text‹

We use the standard continuation monad to ease the semantic
definition.

›

definition unitK :: "'o ValK  'o ValKM" where
  "unitK  Λ a. Λ c. ca"

definition bindK :: "'o ValKM  ('o ValK  'o ValKM)  'o ValKM" where
  "bindK  Λ m k. Λ c. m(Λ a. kac)"

definition appKM :: "'o ValKM  'o ValKM  'o ValKM" where
  "appKM  Λ fK xK. bindKfK(Λ (ValKFf). fxK)"
(*<*)

lemma unitK_simps [simp]:
  "unitKvc = cv"
  unfolding unitK_def by simp

lemma bindK_strict:
  "bindK = "
  unfolding bindK_def by (simp add: eta_cfun)

lemma bindK_unitl:
  "bindK(unitKe)f = fe"
  unfolding bindK_def unitK_def by (simp add: eta_cfun)

lemma bindK_unitr:
  "bindKeunitK = e"
  unfolding bindK_def unitK_def by (simp add: eta_cfun)

lemma bindK_assoc:
  "bindK(bindKfg)h = bindKf(Λ v. bindK(gv)h)"
  unfolding bindK_def unitK_def by simp

lemmas bindK_simps[simp] = bindK_strict bindK_unitl bindK_unitr bindK_assoc

(*>*)
text‹The interpretations of the constants.›

definition
  condK :: "'o ValKM  'o ValKM  'o ValKM  'o ValKM"
where
  "condK  Λ iK tK eK. bindKiK(Λ i. case i of
                ValKFf   | ValKTT  tK | ValKFF  eK | ValKNn  )"

definition succK :: "'o ValKM  'o ValKM" where
  "succK  Λ nK. bindKnK(Λ (ValKNn). unitK(ValKN(n + 1)))"

definition predK :: "'o ValKM  'o ValKM" where
  "predK  Λ nK. bindKnK(Λ (ValKNn). case n of 0   | Suc n  unitK(ValKNn))"

definition isZeroK :: "'o ValKM  'o ValKM" where
  "isZeroK  Λ nK. bindKnK(Λ (ValKNn). unitK(if n = 0 then ValKTT else ValKFF))"

text ‹

A continuation semantics for PCF. If we had defined our direct
semantics using a monad then the correspondence would be more
syntactically obvious.

›

type_synonym 'o EnvK = "'o ValKM Env"

primrec
  evalK :: "expr  'o EnvK  'o ValKM"
where
  "evalK (Var v) = (Λ ρ. ρv)"
| "evalK (App f x) = (Λ ρ. appKM(evalK fρ)(evalK xρ))"
| "evalK (AbsN v e) = (Λ ρ. unitK(ValKF(Λ x. evalK e(env_extvxρ))))"
| "evalK (AbsV v e) = (Λ ρ. unitK(ValKF(Λ x c. x(Λ x'. evalK e(env_extv(unitKx')ρ)c))))"
| "evalK (Diverge) = (Λ ρ. )"
| "evalK (Fix v e) = (Λ ρ. μ x. evalK e(env_extvxρ))"
| "evalK (tt) = (Λ ρ. unitKValKTT)"
| "evalK (ff) = (Λ ρ. unitKValKFF)"
| "evalK (Cond i t e) = (Λ ρ. condK(evalK iρ)(evalK tρ)(evalK eρ))"
| "evalK (Num n) = (Λ ρ. unitK(ValKNn))"
| "evalK (Succ e) = (Λ ρ. succK(evalK eρ))"
| "evalK (Pred e) = (Λ ρ. predK(evalK eρ))"
| "evalK (IsZero e) = (Λ ρ. isZeroK(evalK eρ))"

text‹

To establish the chain completeness (admissibility) of our logical
relation, we need to show that @{term "unitK"} is an \emph{order
monic}, i.e., if @{term "unitKx  unitKy"} then @{term "x 
y"}. This is an order-theoretic version of injectivity.

In order to define a continuation that witnesses this, we need to be
able to distinguish converging and diverging computations. We
therefore require our observation domain to contain at least two
elements:

›

locale at_least_two_elements =
  fixes some_non_bottom_element :: "'o::domain"
  assumes some_non_bottom_element: "some_non_bottom_element  "

text‹

Following citet"DBLP:conf/icalp/Reynolds74" and citet‹Remark
47› in "DBLP:journals/tcs/Filinski07" we use the following continuation:

›

lemma cont_below [simp, cont2cont]:
  "cont (λx::'a::pcpo. if x  d then  else c)"
(*<*)
proof(rule contI2)
  show "monofun (λx. if x  d then  else c)"
    apply (rule monofunI)
    apply clarsimp
    apply (cut_tac x=x and y=y and z=d in below_trans)
    apply auto
    done
next
  fix Y :: "nat  'a::pcpo"
  assume Y: "chain Y"
  assume "chain (λi. if Y i  d then  else c)"
  show "(if ( i. Y i)  d then  else c)  ( i. if Y i  d then  else c)"
  proof(cases "i. Y i  d")
    case True hence "Lub Y  d"
      using lub_below_iff[OF Y] by simp
    thus ?thesis by simp
  next
    case False
    let ?f = "λi. if Y i  d then  else c"
    from False have LubY: "¬ Lub Y  d"
      using lub_below_iff[OF Y] by simp
    from False have F: "chain ?f"
      apply -
      apply (rule chainI)
      apply clarsimp
      apply (cut_tac i=i and j="Suc i" in chain_mono[OF Y])
      apply clarsimp
      apply (cut_tac x="Y i" and y="Y (Suc i)" and z=d in below_trans)
      apply simp_all
      done
    from False obtain i where Yi: "¬ Y i  d" by blast
    hence M: "max_in_chain i ?f"
      apply -
      apply (rule max_in_chainI)
      apply clarsimp
      apply (drule chain_mono[OF Y])
      apply (cut_tac x="Y i" and y="Y j" and z=d in below_trans)
      apply simp_all
      done
    from LubY Yi show ?thesis
      using iffD1[OF maxinch_is_thelub, OF F M] by simp
  qed
qed
(*>*)
text‹›

lemma (in at_least_two_elements) below_monic_unitK [intro, simp]:
  "below_monic_cfun (unitK :: 'o ValK  'o ValKM)"
proof(rule below_monicI)
  fix v v' :: "'o ValK"
  assume vv': "unitKv  unitKv'"
  let ?k = "Λ x. if x  v' then  else some_non_bottom_element"
  from vv' have "unitKv?k  unitKv'?k" by (rule monofun_cfun_fun)
  hence "?kv  ?kv'" by (simp add: unitK_def)
  with some_non_bottom_element show "v  v'" by (auto split: if_split_asm)
qed


subsection‹Logical relation›

text‹

We follow citet"DBLP:conf/icalp/Reynolds74" by simultaneously
defining a pair of relations over values and functions. Both are
bottom-reflecting, in contrast to the situation for computational
adequacy in \S\ref{sec:compad}.  citet"DBLP:journals/tcs/Filinski07"
differs by assuming that values are always defined, and relates values
and monadic computations.

›

type_synonym 'o lfr = "(ValD, 'o ValKM, ValD  ValD, 'o ValKM  'o ValKM) lf_pair_rep"
type_synonym 'o lflf = "(ValD, 'o ValKM, ValD  ValD, 'o ValKM  'o ValKM) lf_pair"

context at_least_two_elements
begin

abbreviation lr_eta_rep_N where
  "lr_eta_rep_N  { (e, e') .
       (e =   e' = )
      (e = ValTT  e' = unitKValKTT)
      (e = ValFF  e' = unitKValKFF)
      (n. e = ValNn  e' = unitK(ValKNn)) }"

abbreviation lr_eta_rep_F where
  "lr_eta_rep_F  λ(rm, rp). { (e, e') .
       (e =   e' = )
      (f f'. e = ValFf  e' = unitK(ValKFf')  (f, f')  unlr (snd rp)) }"

definition lr_eta_rep where
  "lr_eta_rep  λr. lr_eta_rep_N  lr_eta_rep_F r"

definition lr_theta_rep where
  "lr_theta_rep  λ(rm, rp). { (f, f') .
     ((x, x')  unlr (fst (undual rm)). (fx, f'x')  unlr (fst rp)) }"

definition lr_rep :: "'o lfr" where
  "lr_rep  λr. (lr_eta_rep r, lr_theta_rep r)"

abbreviation lr :: "'o lflf" where
  "lr  λr. (mklr (fst (lr_rep r)), mklr (snd (lr_rep r)))"
(*<*)
text‹

Properties of the logical relation.

›

lemma admS_eta_rep [intro, simp]:
  "fst (lr_rep r)  admS"
  unfolding lr_rep_def lr_eta_rep_def
  apply simp
  apply rule
  apply (auto intro!: adm_disj simp: split_def)
   using adm_below_monic_exists[OF _ below_monic_pair[OF below_monic_ValN below_monic_cfcomp2[OF below_monic_unitK below_monic_ValKN]], where P="λ_. True"]
   apply (simp add: prod_eq_iff)
  using adm_below_monic_exists[OF _ below_monic_pair_split[OF below_monic_ValF below_monic_cfcomp2[OF below_monic_unitK below_monic_ValKF]], where P="λx. x  unlr (snd (snd r))"]
  apply (simp add: prod_eq_iff)
  done

lemma admS_theta_rep [intro, simp]:
  "snd (lr_rep r)  admS"
proof
  show "  snd (lr_rep r)"
    unfolding lr_rep_def lr_theta_rep_def
    by (cases r) simp
next
  show "adm (λx. x  snd (lr_rep r))"
    apply (rule admI)
    unfolding lr_rep_def lr_theta_rep_def
    apply (clarsimp simp: split_def)
    apply (rule admD)
      apply (rule adm_subst)
      apply force+
    done
qed

lemma mono_lr:
  shows "mono (lr :: 'o lflf)"
  apply (rule monoI)
  apply simp
  apply (simp add: lr_rep_def)
  apply (rule conjI)
   apply (force simp: lr_eta_rep_def split_def dual_less_eq_iff unlr_leq[symmetric])
  (* FIXME stuck with the projections on the product *)
  apply (auto simp: lr_theta_rep_def split_def dual_less_eq_iff unlr_leq[symmetric])
  apply (drule_tac x="(ae, bc)" in bspec)
   apply (case_tac a)
   apply (case_tac ab)
   apply (auto simp: unlr_leq[symmetric])
  done

(*>*)
end (* context at_least_two_elements *)

text‹

It takes some effort to set up the minimal invariant relating the two
pairs of domains. One might hope this would be easier using deflations
(which might compose) rather than ``copy'' functions (which certainly
don't).

We elide these as they are tedious.

›
(*<*)

primrec
  ValD_copy_i :: "nat  ValD  ValD"
where
  "ValD_copy_i 0 = "
| "ValD_copy_i (Suc n) = (Λ v. case v of ValFf  ValF(ValD_copy_i n oo f oo ValD_copy_i n) | ValTT  ValTT | ValFF  ValFF | ValNm  ValNm)"

abbreviation
  "ValD_copy_lub  (i. ValD_copy_i i)"

lemma ValD_copy_chain [intro, simp]:
  "chain ValD_copy_i"
proof(rule chainI)
  fix i show "ValD_copy_i i  ValD_copy_i (Suc i)"
  proof(induct i)
    case (Suc i)
    { fix x
      have "ValD_copy_i (Suc i)x  ValD_copy_i (Suc (Suc i))x"
      proof(cases x)
        case (ValF f) with Suc show ?thesis
          by (clarsimp simp: cfcomp1 cfun_below_iff monofun_cfun)
      qed simp_all }
    thus ?case by (simp add: cfun_below_iff)
  qed simp
qed

lemma ValD_copy_lub_ID:
  "ValD_copy_lub = ID"
proof -
  { fix x :: ValD
    fix i :: nat
    have "ValD_take i(ValD_copy_i i(ValD_take ix)) = ValD_take ix"
    proof (induct i arbitrary: x)
      case (Suc n) thus ?case
        by (cases x) (simp_all add: cfun_map_def)
    qed simp }
  hence "x :: ValD. (i. ValD_take i(ValD_copy_i i(ValD_take ix))) = (i. ValD_take ix)"
    by (blast intro: lub_eq)
  thus ?thesis by (simp add: lub_distribs ValD.lub_take cfun_eq_iff)
qed

text‹

Continuations: we need to ensure the observation type is always the
same.

›

definition
  KM_map :: "('o ValK  'o ValK)  'o ValKM  'o ValKM"
where
  "KM_map  Λ f. cfun_map(cfun_mapfID)ID"

lemma KM_map_id [intro, simp]:
  "KM_mapID = ID"
  unfolding KM_map_def by (simp add: cfun_map_ID)

lemma KM_map_strict [intro, simp]:
  "KM_mapf = "
  unfolding KM_map_def by (simp add: cfun_map_def)

primrec
  ValK_copy_i :: "nat  'o ValK  'o ValK"
where
  "ValK_copy_i 0 = "
| "ValK_copy_i (Suc n) = (Λ v. case v of ValKFf  ValKF(cfun_map(KM_map(ValK_copy_i n))(KM_map(ValK_copy_i n))f) | ValKTT  ValKTT | ValKFF  ValKFF | ValKNm  ValKNm)"

abbreviation
  "ValK_copy  (i. ValK_copy_i i)"

lemma ValK_copy_chain [intro, simp]:
  "chain (ValK_copy_i :: nat  'o ValK  'o ValK)"
proof(rule chainI)
  fix i show "ValK_copy_i i  (ValK_copy_i (Suc i) :: 'o ValK  'o ValK)"
  proof(induct i)
    case (Suc i)
    { fix x :: "'o ValK"
      have "ValK_copy_i (Suc i)x  ValK_copy_i (Suc (Suc i))x"
      proof(cases x)
        case (ValKF f) with Suc show ?thesis by (clarsimp simp: monofun_cfun KM_map_def)
      qed simp_all }
    thus ?case by (simp add: cfun_below_iff)
  qed simp
qed

lemma ValK_copy_fix:
  "ValK_copy = (ID :: 'o ValK  'o ValK)"
proof -
  { fix x :: "'o ValK"
    fix i :: nat
    have "ValK_take i(ValK_copy_i i(ValK_take ix)) = ValK_take ix"
    proof (induct i arbitrary: x)
      case (Suc n) thus ?case
        by (cases x) (simp_all add: KM_map_def cfun_map_def)
    qed simp }
  hence "x :: 'o ValK. (i. ValK_take i(ValK_copy_i i(ValK_take ix))) = (i. ValK_take ix)"
    by (blast intro: lub_eq)
  thus ?thesis by (simp add: lub_distribs ValK.lub_take cfun_eq_iff)
qed

lemma ValK_strict [intro, simp]:
  "ValK_copy = "
  by (simp add: ValK_copy_fix)

text‹

We need to respect the purported domain structure, and positive and
negative occurrences.

›

fixrec
  ValD_copy_rec :: "((ValD  ValD) × ((ValD  ValD)  (ValD  ValD)))
                   ((ValD  ValD) × ((ValD  ValD)  (ValD  ValD)))"
where
  "ValD_copy_recr =
     (Λ v. case v of ValFf  ValF(snd rf) | ValTT  ValTT | ValFF  ValFF | ValNn  ValNn,
      Λ f. cfun_map(strictify(fst r))(strictify(fst r))f)"

abbreviation
  ValD_copy_eta :: "nat  ValD  ValD"
where
  "ValD_copy_eta i  fst (iterate iValD_copy_rec)"

abbreviation
  ValD_copy_theta :: "nat  (ValD  ValD)  (ValD  ValD)"
where
  "ValD_copy_theta i  snd (iterate iValD_copy_rec)"

lemma ValD_copy_eta_theta_strict [intro, simp]:
  "ValD_copy_eta n = "
  "ValD_copy_theta n = "
  by (induct n) (simp_all add: cfun_map_def)

lemma ValD_copy_fix_strict [simp]:
  "fst (fixValD_copy_rec) = "
  "snd (fixValD_copy_rec) = "
  by (subst fix_eq, simp add: cfun_map_def)+

lemma ValD_copy_rec_ValD_copy_lub:
  "fixValD_copy_rec = (ValD_copy_lub, cfun_mapValD_copy_lubValD_copy_lub)" (is "?lhs = ?rhs")
proof(rule below_antisym)
  show "?lhs  ?rhs"
    apply (rule fix_least)
    apply (simp add: eta_cfun strictify_cancel ValD_copy_lub_ID cfun_map_def ID_def)
    done
next
  { fix i have "ValD_copy_i i  fst (fixValD_copy_rec)"
    proof(induct i)
      case (Suc i) thus ?case
        apply -
        apply (subst fix_eq)
        apply (subst fix_eq)
        apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def)
        apply (intro monofun_cfun_fun monofun_cfun_arg)
        apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def cfun_below_iff)
        done
    qed simp }
  hence D: "ValD_copy_lub  fst (fixValD_copy_rec)" by (simp add: lub_below_iff)
  moreover
  from D
  have "cfun_mapValD_copy_lubValD_copy_lub  snd (fixValD_copy_rec)"
    by (subst fix_eq) (simp add: eta_cfun strictify_cancel monofun_cfun)
  ultimately show "?rhs  ?lhs" by (simp add: prod_belowI)
qed

lemma fix_ValD_copy_rec_ID:
  "fixValD_copy_rec = (ID, ID)"
  using ValD_copy_rec_ValD_copy_lub ValD_copy_lub_ID cfun_map_ID
  by simp

fixrec
  ValK_copy_rec :: "(('o ValKM  'o ValKM) × (('o ValKM  'o ValKM)  ('o ValKM  'o ValKM)))
                   ('o ValKM  'o ValKM) × (('o ValKM  'o ValKM)  ('o ValKM  'o ValKM))"
where
  "ValK_copy_recr =
     (Λ vm. KM_map(Λ v. case v of ValKFf  ValKF(snd rf) | ValKTT  ValKTT | ValKFF  ValKFF | ValKNa  ValKNa)vm,
      Λ f. cfun_map(strictify(fst r))(strictify(fst r))f)"

abbreviation
  ValK_copy_eta
where
  "ValK_copy_eta i  fst (iterate iValK_copy_rec)"

abbreviation
  ValK_copy_theta
where
  "ValK_copy_theta i  snd (iterate iValK_copy_rec)"

lemma ValK_copy_strict [intro, simp]:
  "ValK_copy_eta n = ( :: 'o ValKM)"
  "ValK_copy_theta n = ( :: 'o ValKM  'o ValKM)"
  by (induct n) (simp_all add: cfun_map_def)

lemma ValK_copy_fix_strict [simp]:
  "fst (fixValK_copy_rec) = "
  "snd (fixValK_copy_rec) = "
  by (subst fix_eq, simp add: cfun_map_def)+

lemma ValK_copy_rec_ValK_copy:
  "fixValK_copy_rec
  = (KM_map(ValK_copy :: 'o ValK  'o ValK),
     cfun_map(KM_mapValK_copy)(KM_mapValK_copy))" (is "?lhs = ?rhs")
proof(rule below_antisym)
  show "?lhs  ?rhs"
    apply (rule fix_least)
    apply (simp add: eta_cfun strictify_cancel cfun_map_def ID_def)
    apply (intro cfun_eqI)
    apply (simp add: KM_map_def cfun_map_def ValK_copy_fix eta_cfun)
    done
next
  { fix i
    have "KM_map(ValK_copy_i i :: 'o ValK  'o ValK)  fst (fixValK_copy_rec)"
     and "(ValK_copy_i i :: 'o ValK  'o ValK)  ValK_case(Λ f. ValKF(snd (fixValK_copy_rec)f))ValKTTValKFFValKN"
    proof(induct i)
      case 0
      { case 1 show ?case
          apply (subst fix_eq)
          apply (auto iff: cfun_below_iff intro!: monofun_cfun_arg simp: KM_map_def cfun_map_def eta_cfun)
          done }
      { case 2 show ?case by simp }
    next
      case (Suc i)
      { case 1 from Suc show ?case
          apply -
          apply (subst fix_eq)
          apply (subst fix_eq)
          apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
          apply (intro cfun_belowI)
          apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
          apply (intro monofun_cfun_arg)
          apply (intro cfun_belowI)
          apply (simp add: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def)
          apply (intro monofun_cfun_arg)
          apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def)
          apply (intro monofun_cfun)
          apply simp_all
          apply (intro cfun_belowI)
          apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 cfun_map_def)
          apply (intro cfun_belowI)
          apply (subst fix_eq)
          apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 KM_map_def cfun_map_def)
          apply (intro monofun_cfun)
          apply simp_all
          apply (subst fix_eq)
          apply (intro cfun_belowI)
          apply (simp add: eta_cfun strictify_cancel monofun_cfun cfcomp1 KM_map_def cfun_map_def)
          apply (intro monofun_cfun)
          apply simp_all
          apply (intro cfun_belowI)
          apply simp
          apply (intro monofun_cfun)
          apply simp_all
          apply (intro cfun_belowI)
          apply simp
          apply (intro monofun_cfun)
          apply simp_all
          done }
      { case 2 from Suc show ?case
          apply -
          apply (subst fix_eq)
          apply (subst fix_eq)
          apply (auto simp: eta_cfun strictify_cancel cfcomp1 cfun_map_def KM_map_def cfun_below_iff intro!: monofun_cfun)
          done }
    qed }
  hence "(i. KM_map(ValK_copy_i i :: 'o ValK  'o ValK))  fst (fixValK_copy_rec)"
    by (simp add: lub_below_iff)
  hence D: "KM_map(ValK_copy :: 'o ValK  'o ValK)  fst (fixValK_copy_rec)"
    by (simp add: contlub_cfun_arg[symmetric])
  from D
  have E: "cfun_map(KM_map(ValK_copy :: 'o ValK  'o ValK))(KM_mapValK_copy)  snd (fixValK_copy_rec)"
    apply (subst fix_eq)
    apply (simp add: eta_cfun strictify_cancel KM_map_def)
    apply (intro monofun_cfun)
    apply simp_all
    done
  show "?rhs  ?lhs" by (simp add: prod_belowI D E)
qed

lemma fix_ValK_copy_rec_ID:
  "fixValK_copy_rec = (ID, ID)"
  by (simp add: ValK_copy_rec_ValK_copy ValK_copy_fix cfun_map_ID)

lemma (in at_least_two_elements) min_inv_lr:
  assumes "fst ea = "
  assumes "fst eb = "
  assumes "eRSP ea eb R S"
  shows "eRSP (ValD_copy_recea) (ValK_copy_receb) (dual ((lr :: 'o lflf) (dual S, undual R))) (lr (R, S))"
  using assms some_non_bottom_element
  apply (simp add: split_def)
  apply (auto simp: split_def lr_rep_def lr_eta_rep_def lr_theta_rep_def KM_map_def cfun_map_def unitK_def)
  apply (force simp: cfun_map_def strictify_cancel unitK_def) (* FIXME obvious but auto misses it *)
  done

(*>*)
sublocale at_least_two_elements < F: DomSolP lr ValD_copy_rec ValK_copy_rec
  apply standard
         apply (rule mono_lr)
        apply (rule fix_ValD_copy_rec_ID)
       apply (rule fix_ValK_copy_rec_ID)
      apply (simp_all add: cfun_map_def)[4]
  apply (erule (2) min_inv_lr)
  done


subsection‹A retraction between the two definitions›

text‹

We can use the relation to establish a strong connection between the
direct and continuation semantics.  All results depend on the
observation type being rich enough.

›

context at_least_two_elements
begin

abbreviation mrel ("η: _  _" [50, 51] 50) where
  "η: x  x'  (x, x')  unlr (fst F.delta)"

abbreviation vrel ("θ: _  _" [50, 51] 50) where
  "θ: y  y'  (y, y')  unlr (snd F.delta)"
(*<*)
lemma F_bottom_triv [intro, simp]:
  "η:   "
  "θ:   "
  by simp_all

lemma etaI [intro, simp]:
  "η: ValTT  unitKValKTT"
  "η: ValFF  unitKValKFF"
  "η: ValNn  unitK(ValKNn)"
  by (subst F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)+

lemma eta_F:
  "θ: f  f'  η: ValFf  unitK(ValKFf')"
apply (subst F.delta_sol)
apply simp
apply (subst lr_rep_def)
apply (fastforce simp: lr_eta_rep_def split_def)
done

lemma theta_F:
  "(x x'. η: x  x'  η: fx  f'x')  θ: f  f'"
apply (subst F.delta_sol)
apply simp
apply (subst lr_rep_def)
apply (simp add: lr_theta_rep_def split_def)
done

lemma eta_induct[case_names bottom N F, consumes 1]:
  " η: x  x';
      x = ; x' =    P x x';
     n.  x = ValTT; x' = unitKValKTT   P x x';
     n.  x = ValFF; x' = unitKValKFF   P x x';
     n.  x = ValNn; x' = unitK(ValKNn)   P x x';
     f f'.  x = ValFf; x' = unitK(ValKFf'); θ: f  f'   P x x'
     P x x'"
  apply (cases x)
      apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
     defer
     apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
    apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
   apply (subst (asm) F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)
  apply simp
  apply (subst (asm) F.delta_sol)
  apply simp
  apply (subst (asm) lr_rep_def)
  apply (subst (asm) lr_eta_rep_def)
  apply clarsimp
  done

lemma theta_induct[case_names F, consumes 1]:
  " θ: f  f';
     (x x'. η: x  x'  η: fx  f'x')  P f f'
     P f f'"
  apply (subst (asm) F.delta_sol)
  apply simp
  apply (subst (asm) lr_rep_def)
  apply (subst (asm) lr_theta_rep_def)
  apply fastforce
  done

(*>*)
text‹

Theorem 1 from citet"DBLP:conf/icalp/Reynolds74".

›

lemma AbsV_aux:
  assumes "η: ValFf  unitK(ValKFf')"
  shows "η: ValF(strictifyf)  unitK(ValKF(Λ x c. x(Λ x'. f'(unitKx')c)))"
(*<*)
  apply (rule eta_F)
  apply (rule theta_F)
  using assms
  apply (rule eta_induct) (* FIXME special rule would help *)
  apply simp_all
  apply (drule injD[OF below_monic_inj[OF below_monic_unitK]])
  apply clarsimp
  apply (erule theta_induct)
  apply (erule eta_induct)
  apply (simp_all add: eta_cfun eta_F)
  done

(*>*)
text‹›

theorem Theorem1:
  assumes "v. η: ρv  ρ'v"
  shows "η: evalD eρ  evalK eρ'"
(*<*)
using assms
proof(induct e arbitrary: ρ ρ')
  case App show ?case
    apply simp
    apply (simp add: appKM_def bindK_def)
    using App.hyps(1)[OF App(3)]
    apply (rule eta_induct)
      apply simp_all
    apply (simp add: eta_cfun)
    apply (erule theta_induct)
    using App.hyps(2)[OF App(3)]
    apply simp
    done
next
  case AbsN show ?case
    apply simp
    apply (rule eta_F)
    apply (rule theta_F)
    apply simp
    apply (rule AbsN.hyps)
    using AbsN(2)
    unfolding env_ext_def
    apply simp
    done
next
  case (AbsV v e ρ ρ')
  have "η: ValF(Λ x. evalD e(env_extvxρ))  unitK(ValKF(Λ x. evalK e(env_extvxρ')))"
    apply (rule eta_F)
    apply (rule theta_F)
    apply simp
    apply (rule AbsV.hyps)
    using AbsV(2)
    unfolding env_ext_def
    apply simp
    done
  thus ?case by (fastforce dest: AbsV_aux)
next
  case Fix thus ?case
    apply simp
    apply (rule parallel_fix_ind)
    apply (simp_all add: env_ext_def)
    done
next
  case Cond thus ?case
    apply (simp add: cond_def condK_def eta_cfun)
    using Cond(1)[OF Cond(4)]
    apply (rule eta_induct)
    apply simp_all
    done
next
  case Succ thus ?case
    apply (simp add: succ_def succK_def eta_cfun)
    using Succ(1)[OF Succ(2)]
    apply (rule eta_induct)
    apply simp_all
    done
next
  case Pred thus ?case
    apply (simp add: pred_def predK_def eta_cfun)
    using Pred(1)[OF Pred(2)]
    apply (rule eta_induct)
    apply (simp_all split: nat.split)
    done
next
  case IsZero thus ?case
    apply (simp add: isZero_def isZeroK_def eta_cfun)
    using IsZero(1)[OF IsZero(2)]
    apply (rule eta_induct)
    apply (simp_all split: nat.split)
    done
qed simp_all
(*>*)

end


text‹

The retraction between the two value and monadic value spaces.

Note we need to work with an observation type that can represent the
``explicit values'', i.e. @{typ "'o ValK"}.

›

locale value_retraction =
  fixes VtoO :: "'o ValK  'o"
  fixes OtoV :: "'o  'o ValK"
  assumes OV: "OtoV oo VtoO = ID"

sublocale value_retraction < at_least_two_elements "VtoO(ValKN0)"
using OV by - (standard, simp add: injection_defined cfcomp1 cfun_eq_iff)

context value_retraction
begin

fun
  DtoKM_i :: "nat  ValD  'o ValKM"
and
  KMtoD_i :: "nat  'o ValKM  ValD"
where
  "DtoKM_i 0 = "
| "DtoKM_i (Suc n) = (Λ v. case v of
     ValFf  unitK(ValKF(cfun_map(KMtoD_i n)(DtoKM_i n)f))
   | ValTT  unitKValKTT
   | ValFF  unitKValKFF
   | ValNm  unitK(ValKNm))"

| "KMtoD_i 0 = "
| "KMtoD_i (Suc n) = (Λ v. case OtoV(vVtoO) of
     ValKFf  ValF(cfun_map(DtoKM_i n)(KMtoD_i n)f)
   | ValKTT  ValTT
   | ValKFF  ValFF
   | ValKNm  ValNm)"

abbreviation "DtoKM  (i. DtoKM_i i)"
abbreviation "KMtoD  (i. KMtoD_i i)"
(*<*)

lemma DtoKM_KMtoD_chain [intro, simp]:
  "chain DtoKM_i"
  "chain KMtoD_i"
proof -
  let ?C = "λi. (DtoKM_i i, KMtoD_i i)"
  have "chain ?C"
  proof(rule chainI)
    fix i show "?C i  ?C (Suc i)"
    proof(induct i)
      case (Suc i) show ?case
      proof(rule monofun_pair)
        show "DtoKM_i (Suc i)  DtoKM_i (Suc (Suc i))"
        proof(rule cfun_belowI)
          fix x from Suc show "DtoKM_i (Suc i)x  DtoKM_i (Suc (Suc i))x"
            by (cases x) (auto intro!: monofun_cfun simp: cfun_map_def cfun_below_iff)
        qed
        show "KMtoD_i (Suc i)  KMtoD_i (Suc (Suc i))"
        proof(rule cfun_belowI)
          fix x from Suc show "KMtoD_i (Suc i)x  KMtoD_i (Suc (Suc i))x"
            apply (simp add: eta_cfun)
            apply (intro monofun_cfun_fun monofun_cfun_arg)
            apply (intro cfun_belowI)
            apply (auto intro: monofun_cfun)
            done
        qed
      qed
    qed simp
  qed
  then show "chain DtoKM_i" "chain KMtoD_i"
    by (auto dest: ch2ch_fst ch2ch_snd)
qed
(*>*)

text‹

Lemma 1 from citet"DBLP:conf/icalp/Reynolds74".

›

lemma Lemma1:
  "η: x  DtoKMx"
  "η: x  x'  x = KMtoDx'"
(*<*)
proof -
  have K: "η: ValD_copy_i ix  DtoKM_i ix"
   and L: "η: x  x'  ValD_copy_i ix = KMtoD_i ix'" for x x' i
  proof(induct i arbitrary: x x')
    case (Suc i)
    { case 1 show ?case
        apply (cases x)
          apply simp_all
        apply (rule eta_F)
        apply (rule theta_F)
        using Suc
        apply simp
        done }
    { case 2 thus ?case
        apply (induct rule: eta_induct)
          using OV
          apply (simp_all add: cfun_eq_iff retraction_strict)
        apply (clarsimp simp: cfun_eq_iff)
        apply (erule theta_induct)
        using Suc
        apply simp
        done }
  qed simp_all
  let ?C1 = "λi. (ValD_copy_i i, DtoKM_i i)"
  let ?P1 = "λf. η: (fst f)x  (snd f)x"
  have "adm ?P1" by (rule adm_subst) simp_all
  with K
  have "?P1 (i. ValD_copy_i i, i. DtoKM_i i)"
    using admD[where P="?P1" and Y="?C1"] lub_prod[where S="?C1"] by simp
  moreover
  { fix x :: ValD
    fix x' :: "'o ValKM"
    let ?C2 = "λi. (ValD_copy_i i, KMtoD_i i)"
    let ?P2 = "λf. (fst f)x = (snd f)x'"
    have "adm (λf. ?P2 f)" by simp
    with L have "η: x  x'  ?P2 (i. ValD_copy_i i, i. KMtoD_i i)"
      using admD[where P="?P2" and Y="?C2"] lub_prod[where S="?C2"]
      by simp }
  ultimately show
    "η: x  DtoKMx"
    "η: x  x'  x = KMtoDx'"
      by (simp_all add: ValD_copy_lub_ID)
qed

(*>*)
text‹

Theorem 2 from citet"DBLP:conf/icalp/Reynolds74".

›

theorem Theorem2: "evalD eρ = KMtoD(evalK e(DtoKM oo ρ))"
using Lemma1(2)[OF Theorem1] Lemma1(1) by (simp add: cfcomp1)

end

textcitet‹Remark~48› in "DBLP:journals/tcs/Filinski07" observes that there
will not be a retraction between direct and continuation semantics for
languages with richer notions of effects.

It should be routine to extend the above approach to the higher-order
backtracking language of citet"DBLP:conf/icfp/WandV04".

I wonder if it is possible to construct continuation semantics from
direct semantics as proposed by
citet"DBLP:journals/jacm/SethiT80". Roughly we might hope to lift a
retraction between two value domains to a retraction at higher types
by synthesising a suitable logical relation.

›
(*<*)

end
(*>*)