Quelle  Logical_Relations.thy

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

section ‹Pitts's method for solving recursive domain predicates›
(*<*)

theory Logical_Relations
imports
  Basis
begin

(*>*)
text‹

  adopt the general theory of 🍋‹"PittsAM:relpod"› for solving
  domain predicates. This is based on the idea of
 emph{minimal invariants} that 🍋‹‹Def 2› in "DBLP:conf/mfps/Pitts93"›
  ``essentially to D. Scott''.

  we would like to do the proofs once and use Pitts's
 emph{relational structures}. Unfortunately it seems we need
 -order polymorphism (type functions) to make this work (but see
 🍋‹"Huffman:MonadTransformers:2012"›). Here we develop three
 , one for each of our applications. The proofs are similar
 but not quite identical) in all cases.

  begin by defining an \emph{admissible} set (aka an \emph{inclusive
 }) to be one that contains @{term "⊥"} and is closed under
  chains:

 ›

definition admS :: "'a::pcpo set set" where
  "admS ≡ { R :: 'a set. ⊥ ∈ R ∧ adm (λx. x ∈ R) }"

typedef ('a::pcpo) admS = "{ x::'a::pcpo set . x ∈ admS }"
  morphisms unlr mklr unfolding admS_def by fastforce

text‹

  sets form a complete lattice.

 ›
(*<*)

lemma admSI [intro]:
  "[ ⊥ ∈ R; adm (λx. x ∈ R) ] ==> R ∈ admS"
unfolding admS_def by simp

lemma bottom_in_unlr [simp]:
  "⊥ ∈ unlr R"
using admS.unlr [of R] by (simp add: admS_def)

lemma adm_unlr [simp]:
  "adm (λx. x ∈ unlr R)"
using admS.unlr [of R] by (simp add: admS_def)

lemma adm_cont_unlr [intro, simp]:
  "cont f ==> adm (λx. f x ∈ unlr r)"
by (erule adm_subst) simp

declare admS.mklr_inverse[simp add]

instantiation admS :: (pcpo) order
begin

definition
  "x ≤ y ≡ unlr x ⊆ unlr y"

definition
  "x < y ≡ unlr x ⊂ unlr y"

instance
  by standard (auto simp add: less_eq_admS_def less_admS_def admS.unlr_inject)

end

lemma mklr_leq [iff]: "[ x ∈ admS; y ∈ admS ] ==> (mklr x ≤ mklr y) ⟷ (x ≤ y)"
  unfolding less_eq_admS_def by simp

lemma unlr_leq: "(unlr x ≤ unlr y) ⟷ (x ≤ y)"
  unfolding less_eq_admS_def by simp

instantiation admS :: (pcpo) lattice
begin

definition
  "inf f g ≡ mklr (unlr f ∩ unlr g)"

definition
  "sup f g = mklr (unlr f ∪ unlr g)"

lemma unlr_inf: "unlr (inf x y) = unlr x ∩ unlr y"
  unfolding inf_admS_def by (simp add: admS_def)

lemma unlr_sup: "unlr (sup x y) = unlr x ∪ unlr y"
  unfolding sup_admS_def by (simp add: admS_def)

instance by intro_classes (auto simp: less_eq_admS_def unlr_inf unlr_sup)

end

instantiation admS :: (pcpo) bounded_lattice
begin

definition
  "bot_admS ≡ mklr {⊥}"

lemma unlr_bot[simp]:
  "unlr bot = {⊥}"
  by (simp add: admS_def bot_admS_def)

definition
  "top_admS ≡ mklr UNIV"

instance
proof
  fix x :: "'a admS"
  show "bot ≤ x" by (simp add: bot_admS_def less_eq_admS_def admS_def)
next
  fix x :: "'a admS"
  show "x ≤ top" by (simp add: top_admS_def less_eq_admS_def admS_def)
qed

end

instantiation admS :: (pcpo) complete_lattice
begin

definition
  "Inf A ≡ mklr (Inf (unlr ` A))"

definition
  "Sup (A::'a admS set) = Inf {y. ∀x∈A. x ≤ y}"

lemma mklr_Inf: "unlr (Inf A) = Inf (unlr ` A)"
  unfolding Inf_admS_def by (simp add: admS_def)

lemma INT_admS_bot [simp]:
  "(∩R. unlr R) = {⊥}"
by (auto, metis singletonE unlr_bot)

instance
  by standard
    (auto simp add:
      less_eq_admS_def mklr_Inf Sup_admS_def
      Inf_admS_def bot_admS_def top_admS_def admS_def)

end
(*>*)


subsection‹Sets of vectors›

text‹

  simplest case involves the recursive definition of a set of
  over a single domain. This involves taking the fixed point of
  functor where the \emph{positive} (covariant) occurrences of the
  variable are separated from the \emph{negative}
 contravariant) ones. (See \S\ref{sec:por} etc. for examples.)

  dually ordering the negative uses of the recursion variable the
  is made monotonic with respect to the order on the domain
 {typ "'d"}. Here the type constructor @{typ "'a dual"} yields a type
  the same elements as @{typ "'a"} but with the reverse order. The
  @{term "dual"} and @{term "undual"} mediate the isomorphism.

 ›

type_synonym 'd lf_rep = "'d admS dual × 'd admS ==> 'd set"
type_synonym 'd lf = "'d admS dual × 'd admS ==> 'd admS"

text‹

  predicate @{term "eRSV"} encodes our notion of relation. (This is
 's ‹e : R ⊂ S›.) We model a vector as a function from
  index type @{typ "'i"} to the domain @{typ "'d"}. Note that the
  invariant is for the domain @{typ "'d"} only.

 ›

abbreviation
  eRSV :: "('d::pcpo → 'd) ==> ('i::type ==> 'd) admS dual ==> ('i ==> 'd) admS ==> bool"
where
  "eRSV e R S ≡ ∀d ∈ unlr (undual R). (λx. e⋅(d x)) ∈ unlr S"

text‹

  general we can also assume that @{term "e"} here is strict, but we
  not need to do so for our examples.

  locale captures the key ingredients in Pitts's scheme:
 begin{itemize}

 item that the function @{term "δ"} is a minimal invariant;

 item that the functor defining the relation is suitably monotonic; and

 item that the functor is closed with respect to the minimal invariant.

 end{itemize}

 ›

locale DomSol =
  fixes F :: "'a::order dual × 'a::order ==> 'a"
  assumes monoF: "mono F"
begin

definition sym_lr :: "'a dual × 'a ==> 'a dual × 'a"
where
  "sym_lr = (λ(rm, rp). (dual (F (dual rp, undual rm)), F (rm, rp)))"

lemma sym_lr_mono:
  "mono sym_lr"
proof
  fix x y :: "'a dual × 'a"
  obtain x1 x2 y1 y2 where [simp]: "x = (x1, x2)" "y = (y1, y2)"
    by (cases x, cases y)
  assume "x ≤ y"
  with monoF have "F x ≤ F y" ..
  from ‹x ≤ y› have "(dual y2, undual y1) ≤ (dual x2, undual x1)"
    by (simp_all add: dual_less_eq_iff)
  with monoF have "F (dual y2, undual y1) ≤ F (dual x2, undual x1)" ..
  with ‹F x ≤ F y› show "sym_lr x ≤ sym_lr y"
    by (simp add: sym_lr_def)
qed

end

locale DomSolV = DomSol "F :: ('i::type ==> 'd::pcpo) lf" for F +
  fixes δ :: "('d::pcpo → 'd) → 'd → 'd"
  assumes min_inv_ID: "fix⋅δ = ID"
  assumes eRSV_deltaF:
      "∧(e :: 'd → 'd) (R :: ('i ==> 'd) admS dual) (S :: ('i ==> 'd) admS).
          eRSV e R S ==> eRSV (δ⋅e) (dual (F (dual S, undual R))) (F (R, S))"
(*<*)
context DomSolV
begin

abbreviation
  f_lim :: "('i ==> 'd) admS dual × ('i ==> 'd) admS"
where
  "f_lim ≡ lfp sym_lr"

definition
  delta_neg :: "('i ==> 'd) admS dual"
where
  "delta_neg = fst f_lim"

definition
  delta_pos :: "('i ==> 'd) admS"
where
  "delta_pos = snd f_lim"

lemma delta:
  "(delta_neg, delta_pos) = f_lim"
by (simp add: delta_neg_def delta_pos_def)

lemma delta_neg_sol:
  "delta_neg = dual (F (dual delta_pos, undual delta_neg))"
by (metis (no_types, lifting) case_prod_unfold delta_neg_def delta_pos_def fst_conv lfp_unfold sym_lr_def sym_lr_mono)

lemma delta_pos_sol:
  "delta_pos = F (delta_neg, delta_pos)"
by (metis (no_types, lifting) case_prod_conv delta lfp_unfold snd_conv sym_lr_def sym_lr_mono)

lemma delta_pos_neg_least:
  assumes rm: "rm ≤ F (dual rp, rm)"
  assumes rp: "F (dual rm, rp) ≤ rp"
  shows "delta_neg ≤ dual rm"
    and "delta_pos ≤ rp"
proof -
  from rm rp
  have "(delta_neg, delta_pos) ≤ (dual rm, rp)"
    by (simp add: delta lfp_lowerbound sym_lr_def)
  then show "delta_neg ≤ dual rm" and "delta_pos ≤ rp"
    by simp_all
qed

lemma delta_eq:
  "undual delta_neg = delta_pos"
proof(rule antisym)
  show "delta_pos ≤ undual delta_neg"
    by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
next
  let ?P = "λx. eRSV x (delta_neg) (delta_pos)"
  have "?P (fix⋅δ)"
    by (rule fix_ind, simp_all add: inst_fun_pcpo[symmetric])
       (metis delta_neg_sol delta_pos_sol eRSV_deltaF)
  with min_inv_ID
  show "undual delta_neg ≤ delta_pos"
    by (fastforce simp: unlr_leq[symmetric])
qed
(*>*)
text‹

  these assumptions we can show that there is a unique object that
  a solution to the recursive equation specified by @{term "F"}.

 ›

definition "delta ≡ delta_pos"

lemma delta_sol: "delta = F (dual delta, delta)"
(*<*)
unfolding delta_def
by (subst delta_eq[symmetric], simp, rule delta_pos_sol)
(*>*)

lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
(*<*)
unfolding delta_def
proof(rule antisym)
  show "delta_pos ≤ r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
next
  have "delta_neg ≤ dual r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
  then have "r ≤ undual delta_neg" by (simp add: less_eq_dual_def)
  then show "r ≤ delta_pos"
    using delta_eq by simp
qed
(*>*)

end

text‹

  use this to show certain functions are not PCF-definable in
 S\ref{sec:pcfdefinability}.

 ›

subsection‹Relations between domains and syntax›

text‹

 label{sec:synlr}

  show computational adequacy (\S\ref{sec:compad}) we need to relate
  of a domain to their syntactic counterparts. An advantage of
 's technique is that this is straightforward to do.

 ›

definition synlr :: "('d::pcpo × 'a::type) set set" where
  "synlr ≡ { R :: ('d × 'a) set. ∀a. { d. (d, a) ∈ R } ∈ admS }"

typedef ('d::pcpo, 'a::type) synlr = "{ x::('d × 'a) set. x ∈ synlr }"
  morphisms unsynlr mksynlr unfolding synlr_def by fastforce

text‹

  alternative representation (suggested by Brian Huffman) is to
  use the type @{typ "'a ==> 'b admS"} as this is automatically
  complete lattice. However we end up fighting the automatic methods a
 .

 ›

(*<*)
lemma synlrI [intro]:
  "[ ∧a. (⊥, a) ∈ R; ∧a. adm (λx. (x, a) ∈ R) ] ==> R ∈ synlr"
  unfolding synlr_def by fastforce

lemma bottom_in_unsynlr [simp]:
  "(⊥, a) ∈ unsynlr R"
  using synlr.unsynlr [of R] by (simp add: synlr_def admS_def)

lemma adm_unsynlr [simp]:
  "adm (λx. (x, a) ∈ unsynlr R)"
  using synlr.unsynlr[of R] by (simp add: synlr_def admS_def)

lemma adm_cont_unsynlr [intro, simp]:
  "cont f ==> adm (λx. (f x, a) ∈ unsynlr r)"
  by (erule adm_subst) simp

declare synlr.mksynlr_inverse[simp add]

text‹Lattice machinery.›

instantiation synlr :: (pcpo, type) order
begin

definition
  "x ≤ y ≡ unsynlr x ≤ unsynlr y"

definition
  "x < y ≡ unsynlr x < unsynlr y"

instance
  by standard (auto simp add: less_eq_synlr_def less_synlr_def synlr.unsynlr_inject)

end

lemma mksynlr_leq [iff]: "[ x ∈ synlr; y ∈ synlr ] ==> (mksynlr x ≤ mksynlr y) ⟷ (x ≤ y)"
  unfolding less_eq_synlr_def by simp

lemma unsynlr_leq: "(unsynlr x ≤ unsynlr y) ⟷ (x ≤ y)"
  unfolding less_eq_synlr_def by simp

instantiation synlr :: (pcpo, type) lattice
begin

definition
  "inf f g ≡ mksynlr (unsynlr f ∩ unsynlr g)"

definition
  "sup f g = mksynlr (unsynlr f ∪ unsynlr g)"

lemma unsynlr_inf: "unsynlr (inf x y) = unsynlr x ∩ unsynlr y"
  unfolding inf_synlr_def by (simp add: admS_def synlr_def)

lemma unsynlr_sup: "unsynlr (sup x y) = unsynlr x ∪ unsynlr y"
  unfolding sup_synlr_def by (simp add: admS_def synlr_def)

instance by intro_classes (auto simp: less_eq_synlr_def unsynlr_inf unsynlr_sup)

end

instantiation synlr :: (pcpo, type) bounded_lattice
begin

definition
  "bot_synlr ≡ mksynlr ({⊥} × UNIV)"

lemma unsynlr_bot[simp]:
  "unsynlr bot = {⊥} × UNIV"
  by (simp add: admS_def synlr_def bot_synlr_def)

definition
  "top_synlr ≡ mksynlr UNIV"

instance
proof
  fix x :: "('a, 'b) synlr"
  show "bot ≤ x" by (auto simp: bot_synlr_def less_eq_synlr_def admS_def synlr_def)
next
  fix x :: "('a, 'b) synlr"
  show "x ≤ top" by (auto simp: top_synlr_def less_eq_synlr_def admS_def synlr_def)
qed

end

instantiation synlr :: (pcpo, type) complete_lattice
begin

definition
  "Inf A ≡ mksynlr (Inf (unsynlr ` A))"

definition
  "Sup (A::('a,'b) synlr set) = Inf {y. ∀x∈A. x ≤ y}"

lemma mksynlr_Inf: "unsynlr (Inf A) = Inf (unsynlr ` A)"
  unfolding Inf_synlr_def by (simp add: admS_def synlr_def)

lemma INT_synlr_bot [simp]:
  "(∩R. unsynlr R) = {⊥} × UNIV"
apply auto
apply (drule spec[of _ "mksynlr ({⊥} × UNIV)"])
apply (metis bot_synlr_def mem_Sigma_iff singletonE unsynlr_bot)
done

instance
apply standard
apply (auto simp add: less_eq_synlr_def mksynlr_Inf Sup_synlr_def)
apply (auto simp add: Inf_synlr_def bot_synlr_def top_synlr_def)
done

end

(*>*)
text‹

  we define functors on @{typ "('d, 'a) synlr"}.

 ›

type_synonym ('d, 'a) synlf_rep = "('d, 'a) synlr dual × ('d, 'a) synlr ==> ('d × 'a) set"
type_synonym ('d, 'a) synlf = "('d, 'a) synlr dual × ('d, 'a) synlr ==> ('d, 'a) synlr"

text‹

  capture our relations as before. Note we need the inclusion @{term
 e"} to be strict for our example.

 ›

abbreviation
  eRSS :: "('d::pcpo → 'd) ==> ('d, 'a::type) synlr dual ==> ('d, 'a) synlr ==> bool"
where
  "eRSS e R S ≡ ∀(d, a) ∈ unsynlr (undual R). (e⋅d, a) ∈ unsynlr S"

locale DomSolSyn =  DomSol "F :: ('d::pcpo, 'a::type) synlf" for F +
  fixes δ :: "('d::pcpo → 'd) → 'd → 'd"
  assumes min_inv_ID: "fix⋅δ = ID"
  assumes min_inv_strict: "∧r. δ⋅r⋅⊥ = ⊥"
  assumes eRS_deltaF:
      "∧(e :: 'd → 'd) (R :: ('d, 'a) synlr dual) (S :: ('d, 'a) synlr).
          [ e⋅⊥ = ⊥; eRSS e R S ] ==> eRSS (δ⋅e) (dual (F (dual S, undual R))) (F (R, S))"
(*<*)

context DomSolSyn
begin

abbreviation
  f_lim :: "('d, 'a) synlr dual × ('d, 'a) synlr"
where
  "f_lim ≡ lfp sym_lr"

definition
  delta_neg :: "('d, 'a) synlr dual"
where
  "delta_neg = fst f_lim"

definition
  delta_pos :: "('d, 'a) synlr"
where
  "delta_pos = snd f_lim"

lemma delta:
  "(delta_neg, delta_pos) = f_lim"
by (simp add: delta_neg_def delta_pos_def)

lemma delta_neg_sol:
  "delta_neg = dual (F (dual delta_pos, undual delta_neg))"
by (metis (no_types, lifting) case_prod_unfold delta_neg_def delta_pos_def fst_conv lfp_unfold sym_lr_def sym_lr_mono)

lemma delta_pos_sol:
  "delta_pos = F (delta_neg, delta_pos)"
by (metis (no_types, lifting) case_prod_conv delta lfp_unfold snd_conv sym_lr_def sym_lr_mono)

lemma delta_pos_neg_least:
  assumes rm: "rm ≤ F (dual rp, rm)"
  assumes rp: "F (dual rm, rp) ≤ rp"
  shows "delta_neg ≤ dual rm"
    and "delta_pos ≤ rp"
proof -
  from rm rp
  have "(delta_neg, delta_pos) ≤ (dual rm, rp)"
    by (simp add: delta lfp_lowerbound sym_lr_def)
  then show "delta_neg ≤ dual rm" and "delta_pos ≤ rp"
    by simp_all
qed

lemma delta_eq:
  "undual delta_neg = delta_pos"
proof(rule antisym)
  show "delta_pos ≤ undual delta_neg"
    by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
next
  let ?P = "λx. x⋅⊥ = ⊥ ∧ eRSS x (delta_neg) (delta_pos)"
  have "?P (fix⋅δ)"
    by (rule fix_ind, simp_all)
       (metis delta_neg_sol delta_pos_sol eRS_deltaF min_inv_strict)
  with min_inv_ID
  show "undual delta_neg ≤ delta_pos"
    by (fastforce simp: unsynlr_leq[symmetric])
qed

definition
  "delta ≡ delta_pos"

lemma delta_sol:
  "delta = F (dual delta, delta)"
unfolding delta_def
by (subst delta_eq[symmetric], simp, rule delta_pos_sol)

lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
unfolding delta_def
proof(rule antisym)
  show "delta_pos ≤ r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
next
  have "delta_neg ≤ dual r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
  then have "r ≤ undual delta_neg" by (simp add: less_eq_dual_def)
  then show "r ≤ delta_pos"
    using delta_eq by simp
qed

end

(*>*)
text‹

 , from these assumptions we can construct the unique solution to
  recursive equation specified by @{term "F"}.

 ›

subsection‹Relations between pairs of domains›

text‹

  🍋‹"DBLP:conf/icalp/Reynolds74"› and
 🍋‹"DBLP:journals/tcs/Filinski07"›, we want to relate two pairs of
 -recursive domains. Each of the pairs represents a (monadic)
  and value space.

 ›

type_synonym ('am, 'bm, 'av, 'bv) lr_pair = "('am × 'bm) admS × ('av × 'bv) admS"

type_synonym ('am, 'bm, 'av, 'bv) lf_pair_rep =
  "('am, 'bm, 'av, 'bv) lr_pair dual × ('am, 'bm, 'av, 'bv) lr_pair ==> (('am × 'bm) set × ('av × 'bv) set)"

type_synonym ('am, 'bm, 'av, 'bv) lf_pair =
  "('am, 'bm, 'av, 'bv) lr_pair dual × ('am, 'bm, 'av, 'bv) lr_pair ==> (('am × 'bm) admS × ('av × 'bv) admS)"

text‹

  inclusions need to be strict to get our example through.

 ›

abbreviation
  eRSP :: "(('am::pcpo → 'am) × ('av::pcpo → 'av))
       ==> (('bm::pcpo → 'bm) × ('bv::pcpo → 'bv))
       ==> (('am × 'bm) admS × ('av × 'bv) admS) dual
       ==> ('am × 'bm) admS × ('av × 'bv) admS
       ==> bool"
where
  "eRSP ea eb R S ≡
     (∀(am, bm) ∈ unlr (fst (undual R)). (fst ea⋅am, fst eb⋅bm) ∈ unlr (fst S))
   ∧ (∀(av, bv) ∈ unlr (snd (undual R)). (snd ea⋅av, snd eb⋅bv) ∈ unlr (snd S))"

locale DomSolP = DomSol "F :: ('am::pcpo, 'bm::pcpo, 'av::pcpo, 'bv::pcpo) lf_pair" for F +
  fixes ad :: "(('am → 'am) × ('av → 'av)) → (('am → 'am) × ('av → 'av))"
  fixes bd :: "(('bm → 'bm) × ('bv → 'bv)) → (('bm → 'bm) × ('bv → 'bv))"
  assumes ad_ID: "fix⋅ad = (ID, ID)"
  assumes bd_ID: "fix⋅bd = (ID, ID)"
  assumes ad_strict: "∧r. fst (ad⋅r)⋅⊥ = ⊥" "∧r. snd (ad⋅r)⋅⊥ = ⊥"
  assumes bd_strict: "∧r. fst (bd⋅r)⋅⊥ = ⊥" "∧r. snd (bd⋅r)⋅⊥ = ⊥"
  assumes eRSP_deltaF:
    "[ eRSP ea eb R S; fst ea⋅⊥ = ⊥; snd ea⋅⊥ = ⊥; fst eb⋅⊥ = ⊥; snd ea⋅⊥ = ⊥ ]
      ==> eRSP (ad⋅ea) (bd⋅eb) (dual (F (dual S, undual R))) (F (R, S))"
(*<*)

context DomSolP
begin

abbreviation
  f_lim :: "('am, 'bm, 'av, 'bv) lr_pair dual × ('am, 'bm, 'av, 'bv) lr_pair"
where
  "f_lim ≡ lfp sym_lr"

definition
  delta_neg :: "('am, 'bm, 'av, 'bv) lr_pair dual"
where
  "delta_neg = fst f_lim"

definition
  delta_pos :: "('am, 'bm, 'av, 'bv) lr_pair"
where
  "delta_pos = snd f_lim"

lemma delta:
  "(delta_neg, delta_pos) = f_lim"
by (simp add: delta_neg_def delta_pos_def)

lemma delta_neg_sol:
  "delta_neg = dual (F (dual delta_pos, undual delta_neg))"
by (metis (no_types, lifting) case_prod_unfold delta_neg_def delta_pos_def fst_conv lfp_unfold sym_lr_def sym_lr_mono)

lemma delta_pos_sol:
  "delta_pos = F (delta_neg, delta_pos)"
by (metis (no_types, lifting) case_prod_conv delta lfp_unfold snd_conv sym_lr_def sym_lr_mono)

lemma delta_pos_neg_least:
  assumes rm: "rm ≤ F (dual rp, rm)"
  assumes rp: "F (dual rm, rp) ≤ rp"
  shows "delta_neg ≤ dual rm"
    and "delta_pos ≤ rp"
proof -
  from rm rp
  have "(delta_neg, delta_pos) ≤ (dual rm, rp)"
    by (simp add: delta lfp_lowerbound sym_lr_def)
  then show "delta_neg ≤ dual rm" and "delta_pos ≤ rp"
    by simp_all
qed

lemma delta_eq:
  "undual delta_neg = delta_pos"
proof(rule antisym)
  show "delta_pos ≤ undual delta_neg"
    by (metis delta_neg_sol delta_pos_neg_least(2) delta_pos_sol order_refl undual_dual)
next
  let ?P = "λ(ea, eb). eRSP ea eb (delta_neg) (delta_pos) ∧ fst ea⋅⊥ = ⊥ ∧ snd ea⋅⊥ = ⊥ ∧ fst eb⋅⊥ = ⊥ ∧ snd eb⋅⊥ = ⊥"
  have "?P (fix⋅ad, fix⋅bd)"
    apply (rule parallel_fix_ind)
    apply simp_all
    using ad_strict bd_strict
    apply clarsimp
    apply (cut_tac ea="(a, b)" and eb="(aa, ba)" in eRSP_deltaF[where R=delta_neg and S=delta_pos])
    apply (simp_all add: delta_pos_sol[symmetric])
    apply (subst delta_neg_sol)
    apply simp
    apply (subst delta_neg_sol)
    apply simp
    done
  then have "?P ((ID, ID), (ID, ID))" by (simp only: ad_ID bd_ID)
  then show "undual delta_neg ≤ delta_pos"
    by (fastforce simp: unlr_leq[symmetric] less_eq_prod_def)
qed

definition
  "delta ≡ delta_pos"

lemma delta_sol:
  "delta = F (dual delta, delta)"
unfolding delta_def
by (subst delta_eq[symmetric], simp, rule delta_pos_sol)

lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
unfolding delta_def
proof(rule antisym)
  show "delta_pos ≤ r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
next
  have "delta_neg ≤ dual r"
    using assms delta_pos_neg_least[where rm=r and rp=r] by simp
  then have "r ≤ undual delta_neg" by (simp add: less_eq_dual_def)
  then show "r ≤ delta_pos"
    using delta_eq by simp
qed

end
(*>*)

text‹

  use this solution to relate the direct and continuation semantics
  PCF in \S\ref{sec:continuations}.

 ›
(*<*)

end
(*>*)