Theory Logical_Relations
section ‹Pitts's method for solving recursive domain predicates›
theory Logical_Relations
imports
Basis
begin
text‹
We adopt the general theory of \<^citet>‹"PittsAM:relpod"› for solving
recursive domain predicates. This is based on the idea of
\emph{minimal invariants} that \<^citet>‹‹Def 2› in "DBLP:conf/mfps/Pitts93"›
ascribes ``essentially to D. Scott''.
Ideally we would like to do the proofs once and use Pitts's
\emph{relational structures}. Unfortunately it seems we need
higher-order polymorphism (type functions) to make this work (but see
\<^citet>‹"Huffman:MonadTransformers:2012"›). Here we develop three
versions, one for each of our applications. The proofs are similar
(but not quite identical) in all cases.
We begin by defining an \emph{admissible} set (aka an \emph{inclusive
predicate}) to be one that contains @{term "⊥"} and is closed under
countable 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‹
These 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‹
The simplest case involves the recursive definition of a set of
vectors over a single domain. This involves taking the fixed point of
a functor where the \emph{positive} (covariant) occurrences of the
recursion variable are separated from the \emph{negative}
(contravariant) ones. (See \S\ref{sec:por} etc. for examples.)
By dually ordering the negative uses of the recursion variable the
functor is made monotonic with respect to the order on the domain
@{typ "'d"}. Here the type constructor @{typ "'a dual"} yields a type
with the same elements as @{typ "'a"} but with the reverse order. The
functions @{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‹
The predicate @{term "eRSV"} encodes our notion of relation. (This is
Pitts's ‹e : R ⊂ S›.) We model a vector as a function from
some index type @{typ "'i"} to the domain @{typ "'d"}. Note that the
minimal 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‹
In general we can also assume that @{term "e"} here is strict, but we
do not need to do so for our examples.
Our 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‹
From these assumptions we can show that there is a unique object that
is 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‹
We 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}
To show computational adequacy (\S\ref{sec:compad}) we need to relate
elements of a domain to their syntactic counterparts. An advantage of
Pitts'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‹
An alternative representation (suggested by Brian Huffman) is to
directly use the type @{typ "'a ⇒ 'b admS"} as this is automatically
a complete lattice. However we end up fighting the automatic methods a
lot.
›
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‹
Again 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‹
We capture our relations as before. Note we need the inclusion @{term
"e"} to be strict for our example.
›
abbreviation
:: "('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‹
Again, from these assumptions we can construct the unique solution to
the recursive equation specified by @{term "F"}.
›
subsection‹Relations between pairs of domains›
text‹
Following \<^citet>‹"DBLP:conf/icalp/Reynolds74"› and
\<^citet>‹"DBLP:journals/tcs/Filinski07"›, we want to relate two pairs of
mutually-recursive domains. Each of the pairs represents a (monadic)
computation 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‹
The 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‹
We use this solution to relate the direct and continuation semantics
for PCF in \S\ref{sec:continuations}.
›
end