Quelle  Continuations.thy   Sprache: Isabelle

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

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

(*>*)
text‹

 label{sec:continuations}

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

  begin by giving PCF a continuation semantics following the modern
  of 🚫‹"wadler92:_essence_of_funct_progr"›. We use the
  function space ‹('o ValK, 'o) K → ('o ValK, 'o) K›
  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_case⋅ValKF⋅ValKTT⋅ValKFF⋅ValKN = 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‹

  use the standard continuation monad to ease the semantic
 .

 ›

definition unitK :: "'o ValK → 'o ValKM" where
  "unitK ≡ Λ a. Λ c. c⋅a"

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

definition appKM :: "'o ValKM → 'o ValKM → 'o ValKM" where
  "appKM ≡ Λ fK xK. bindK⋅fK⋅(Λ (ValKF⋅f). f⋅xK)"
(*<*)

lemma unitK_simps [simp]:
  "unitK⋅v⋅c = c⋅v"
  unfolding unitK_def by simp

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

lemma bindK_unitl:
  "bindK⋅(unitK⋅e)⋅f = f⋅e"
  unfolding bindK_def unitK_def by (simp add: eta_cfun)

lemma bindK_unitr:
  "bindK⋅e⋅unitK = e"
  unfolding bindK_def unitK_def by (simp add: eta_cfun)

lemma bindK_assoc:
  "bindK⋅(bindK⋅f⋅g)⋅h = bindK⋅f⋅(Λ v. bindK⋅(g⋅v)⋅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. bindK⋅iK⋅(Λ i. case i of
                ValKF⋅f → ⊥ | ValKTT → tK | ValKFF → eK | ValKN⋅n → ⊥)"

definition succK :: "'o ValKM → 'o ValKM" where
  "succK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). unitK⋅(ValKN⋅(n + 1)))"

definition predK :: "'o ValKM → 'o ValKM" where
  "predK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). case n of 0 → ⊥ | Suc n → unitK⋅(ValKN⋅n))"

definition isZeroK :: "'o ValKM → 'o ValKM" where
  "isZeroK ≡ Λ nK. bindK⋅nK⋅(Λ (ValKN⋅n). unitK⋅(if n = 0 then ValKTT else ValKFF))"

text ‹

  continuation semantics for PCF. If we had defined our direct
  using a monad then the correspondence would be more
  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_ext⋅v⋅x⋅ρ))))"
| "evalK (AbsV v e) = (Λ ρ. unitK⋅(ValKF⋅(Λ x c. x⋅(Λ x'. evalK e⋅(env_ext⋅v⋅(unitK⋅x')⋅ρ)⋅c))))"
| "evalK (Diverge) = (Λ ρ. ⊥)"
| "evalK (Fix v e) = (Λ ρ. μ x. evalK e⋅(env_ext⋅v⋅x⋅ρ))"
| "evalK (tt) = (Λ ρ. unitK⋅ValKTT)"
| "evalK (ff) = (Λ ρ. unitK⋅ValKFF)"
| "evalK (Cond i t e) = (Λ ρ. condK⋅(evalK i⋅ρ)⋅(evalK t⋅ρ)⋅(evalK e⋅ρ))"
| "evalK (Num n) = (Λ ρ. unitK⋅(ValKN⋅n))"
| "evalK (Succ e) = (Λ ρ. succK⋅(evalK e⋅ρ))"
| "evalK (Pred e) = (Λ ρ. predK⋅(evalK e⋅ρ))"
| "evalK (IsZero e) = (Λ ρ. isZeroK⋅(evalK e⋅ρ))"

text‹

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

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

 ›

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

text‹

  🚫‹"DBLP:conf/icalp/Reynolds74"› and 🚫‹‹Remark
 › 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': "unitK⋅v ⊑ unitK⋅v'"
  let ?k = "Λ x. if x ⊑ v' then ⊥ else some_non_bottom_element"
  from vv' have "unitK⋅v⋅?k ⊑ unitK⋅v'⋅?k" by (rule monofun_cfun_fun)
  hence "?k⋅v ⊑ ?k⋅v'" by (simp add: unitK_def)
  with some_non_bottom_element show "v ⊑ v'" by (auto split: if_split_asm)
qed


subsection‹Logical relation›

text‹

  follow 🚫‹"DBLP:conf/icalp/Reynolds74"› by simultaneously
  a pair of relations over values and functions. Both are
 -reflecting, in contrast to the situation for computational
  in \S\ref{sec:compad}. 🚫‹"DBLP:journals/tcs/Filinski07"›
  by assuming that values are always defined, and relates values
  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' = unitK⋅ValKTT)
     ∨ (e = ValFF ∧ e' = unitK⋅ValKFF)
     ∨ (∃n. e = ValN⋅n ∧ e' = unitK⋅(ValKN⋅n)) }"

abbreviation lr_eta_rep_F where
  "lr_eta_rep_F ≡ λ(rm, rp). { (e, e') .
       (e = ⊥ ∧ e' = ⊥)
     ∨ (∃f f'. e = ValF⋅f ∧ e' = unitK⋅(ValKF⋅f') ∧ (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)). (f⋅x, 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‹

  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‹

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

  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 ValF⋅f → ValF⋅(ValD_copy_i n oo f oo ValD_copy_i n) | ValTT → ValTT | ValFF → ValFF | ValN⋅m → ValN⋅m)"

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 i⋅x)) = ValD_take i⋅x"
    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 i⋅x))) = (⊔i. ValD_take i⋅x)"
    by (blast intro: lub_eq)
  thus ?thesis by (simp add: lub_distribs ValD.lub_take cfun_eq_iff)
qed

text‹

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

 ›

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

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

lemma KM_map_strict [intro, simp]:
  "KM_map⋅f⋅⊥ = ⊥"
  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 ValKF⋅f → ValKF⋅(cfun_map⋅(KM_map⋅(ValK_copy_i n))⋅(KM_map⋅(ValK_copy_i n))⋅f) | ValKTT → ValKTT | ValKFF → ValKFF | ValKN⋅m → ValKN⋅m)"

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 i⋅x)) = ValK_take i⋅x"
    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 i⋅x))) = (⊔i. ValK_take i⋅x)"
    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‹

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

 ›

fixrec
  ValD_copy_rec :: "((ValD → ValD) × ((ValD → ValD) → (ValD → ValD)))
                  → ((ValD → ValD) × ((ValD → ValD) → (ValD → ValD)))"
where
  "ValD_copy_rec⋅r =
     (Λ v. case v of ValF⋅f → ValF⋅(snd r⋅f) | ValTT → ValTT | ValFF → ValFF | ValN⋅n → ValN⋅n,
      Λ f. cfun_map⋅(strictify⋅(fst r))⋅(strictify⋅(fst r))⋅f)"

abbreviation
  ValD_copy_eta :: "nat → ValD → ValD"
where
  "ValD_copy_eta i ≡ fst (iterate i⋅ValD_copy_rec⋅⊥)"

abbreviation
  ValD_copy_theta :: "nat → (ValD → ValD) → (ValD → ValD)"
where
  "ValD_copy_theta i ≡ snd (iterate i⋅ValD_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 (fix⋅ValD_copy_rec)⋅⊥ = ⊥"
  "snd (fix⋅ValD_copy_rec)⋅⊥ = ⊥"
  by (subst fix_eq, simp add: cfun_map_def)+

lemma ValD_copy_rec_ValD_copy_lub:
  "fix⋅ValD_copy_rec = (ValD_copy_lub, cfun_map⋅ValD_copy_lub⋅ValD_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 (fix⋅ValD_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 (fix⋅ValD_copy_rec)" by (simp add: lub_below_iff)
  moreover
  from D
  have "cfun_map⋅ValD_copy_lub⋅ValD_copy_lub ⊑ snd (fix⋅ValD_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:
  "fix⋅ValD_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_rec⋅r =
     (Λ vm. KM_map⋅(Λ v. case v of ValKF⋅f → ValKF⋅(snd r⋅f) | ValKTT → ValKTT | ValKFF → ValKFF | ValKN⋅a → ValKN⋅a)⋅vm,
      Λ f. cfun_map⋅(strictify⋅(fst r))⋅(strictify⋅(fst r))⋅f)"

abbreviation
  ValK_copy_eta
where
  "ValK_copy_eta i ≡ fst (iterate i⋅ValK_copy_rec⋅⊥)"

abbreviation
  ValK_copy_theta
where
  "ValK_copy_theta i ≡ snd (iterate i⋅ValK_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 (fix⋅ValK_copy_rec)⋅⊥ = ⊥"
  "snd (fix⋅ValK_copy_rec)⋅⊥ = ⊥"
  by (subst fix_eq, simp add: cfun_map_def)+

lemma ValK_copy_rec_ValK_copy:
  "fix⋅ValK_copy_rec
  = (KM_map⋅(ValK_copy :: 'o ValK → 'o ValK),
     cfun_map⋅(KM_map⋅ValK_copy)⋅(KM_map⋅ValK_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 (fix⋅ValK_copy_rec)"
     and "(ValK_copy_i i :: 'o ValK → 'o ValK) ⊑ ValK_case⋅(Λ f. ValKF⋅(snd (fix⋅ValK_copy_rec)⋅f))⋅ValKTT⋅ValKFF⋅ValKN"
    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 (fix⋅ValK_copy_rec)"
    by (simp add: lub_below_iff)
  hence D: "KM_map⋅(ValK_copy :: 'o ValK → 'o ValK) ⊑ fst (fix⋅ValK_copy_rec)"
    by (simp add: contlub_cfun_arg[symmetric])
  from D
  have E: "cfun_map⋅(KM_map⋅(ValK_copy :: 'o ValK → 'o ValK))⋅(KM_map⋅ValK_copy) ⊑ snd (fix⋅ValK_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:
  "fix⋅ValK_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_rec⋅ea) (ValK_copy_rec⋅eb) (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‹

  can use the relation to establish a strong connection between the
  and continuation semantics. All results depend on the
  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 ↦ unitK⋅ValKTT"
  "η: ValFF ↦ unitK⋅ValKFF"
  "η: ValN⋅n ↦ unitK⋅(ValKN⋅n)"
  by (subst F.delta_sol, simp, simp add: lr_rep_def lr_eta_rep_def)+

lemma eta_F:
  "θ: f ↦ f' ==> η: ValF⋅f ↦ unitK⋅(ValKF⋅f')"
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' ==> η: f⋅x ↦ 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' = unitK⋅ValKTT ] ==> P x x';
     ∧n. [ x = ValFF; x' = unitK⋅ValKFF ] ==> P x x';
     ∧n. [ x = ValN⋅n; x' = unitK⋅(ValKN⋅n) ] ==> P x x';
     ∧f f'. [ x = ValF⋅f; x' = unitK⋅(ValKF⋅f'); θ: 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' ==> η: f⋅x ↦ 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‹

  1 from 🚫‹"DBLP:conf/icalp/Reynolds74"›.

 ›

lemma AbsV_aux:
  assumes "η: ValF⋅f ↦ unitK⋅(ValKF⋅f')"
  shows "η: ValF⋅(strictify⋅f) ↦ unitK⋅(ValKF⋅(Λ x c. x⋅(Λ x'. f'⋅(unitK⋅x')⋅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_ext⋅v⋅x⋅ρ)) ↦ unitK⋅(ValKF⋅(Λ x. evalK e⋅(env_ext⋅v⋅x⋅ρ')))"
    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‹

  retraction between the two value and monadic value spaces.

  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⋅(ValKN⋅0)"
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
     ValF⋅f → unitK⋅(ValKF⋅(cfun_map⋅(KMtoD_i n)⋅(DtoKM_i n)⋅f))
   | ValTT → unitK⋅ValKTT
   | ValFF → unitK⋅ValKFF
   | ValN⋅m → unitK⋅(ValKN⋅m))"

| "KMtoD_i 0 = ⊥"
| "KMtoD_i (Suc n) = (Λ v. case OtoV⋅(v⋅VtoO) of
     ValKF⋅f → ValF⋅(cfun_map⋅(DtoKM_i n)⋅(KMtoD_i n)⋅f)
   | ValKTT → ValTT
   | ValKFF → ValFF
   | ValKN⋅m → ValN⋅m)"

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‹

  1 from 🚫‹"DBLP:conf/icalp/Reynolds74"›.

 ›

lemma Lemma1:
  "η: x ↦ DtoKM⋅x"
  "η: x ↦ x' ==> x = KMtoD⋅x'"
(*<*)
proof -
  have K: "η: ValD_copy_i i⋅x ↦ DtoKM_i i⋅x"
   and L: "η: x ↦ x' ==> ValD_copy_i i⋅x = KMtoD_i i⋅x'" 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 ↦ DtoKM⋅x"
    "η: x ↦ x' ==> x = KMtoD⋅x'"
      by (simp_all add: ValD_copy_lub_ID)
qed

(*>*)
text‹

  2 from 🚫‹"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

text‹

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

  should be routine to extend the above approach to the higher-order
  language of 🚫‹"DBLP:conf/icfp/WandV04"›.

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

 ›
(*<*)

end
(*>*)