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

section ‹Logical relations for definability in PCF›
(*<*)

theory PCF
imports
  Basis
  Logical_Relations
begin

(*>*)
text‹

 label{sec:directsem}

  this machinery we can demonstrate some classical results about
  🚫‹"Plotkin77"›. We diverge from the traditional treatment by
  PCF as an untyped language and including both call-by-name
 CBN) and call-by-value (CBV) abstractions following
 🚫‹"DBLP:conf/icalp/Reynolds74"›. We also adopt some of the
  of 🚫‹‹Chapter~11› in "Winskel:1993"›, in particular by
  the fixed point operator a binding construct.

  model the syntax of PCF as a HOL datatype, where variables have
  drawn from the naturals:

 ›

type_synonym var = nat

datatype expr =
    Var var
  | App expr expr
  | AbsN var expr (* non-strict fns *)
  | AbsV var expr (* strict fns *)
  | Diverge (‹Ω›)
  | Fix var expr
  | tt
  | ff
  | Cond expr expr expr
  | Num nat
  | Succ expr
  | Pred expr
  | IsZero expr

subsection‹Direct denotational semantics›

text‹

 label{sec:densem}

  give this language a direct denotational semantics by interpreting
  into a domain of values.

 ›

domain ValD =
   ValF (lazy appF :: "ValD → ValD")
 | ValTT | ValFF
 | ValN (lazy "nat")

text‹

  \textbf{lazy} keyword means that the @{term "ValF"} constructor is
 , i.e. @{term "ValF⋅⊥ ≠ ⊥"}, which further means that @{term
 ValF⋅(Λ x. ⊥) ≠ ⊥"}.

  naturals are discretely ordered.

 ›
(*<*)

lemma ValD_case_ID [simp]:
  "ValD_case⋅ValF⋅ValTT⋅ValFF⋅ValN = ID"
  apply (rule cfun_eqI)
  apply (case_tac x)
  apply simp_all
  done

lemma below_monic_ValF [iff]:
  "below_monic_cfun ValF"
  by (rule below_monicI) simp

lemma below_monic_ValN [iff]:
  "below_monic_cfun ValN"
  by (rule below_monicI) simp

(*>*)
text‹

  minimal invariant for @{typ "ValD"} is straightforward; the
  @{term "cfun_map⋅f⋅g⋅h"} denotes @{term "g oo h oo f"}.

 ›

fixrec
  ValD_copy_rec :: "(ValD → ValD) → (ValD → ValD)"
where
  "ValD_copy_rec⋅r⋅(ValF⋅f) = ValF⋅(cfun_map⋅r⋅r⋅f)"
| "ValD_copy_rec⋅r⋅(ValTT) = ValTT"
| "ValD_copy_rec⋅r⋅(ValFF) = ValFF"
| "ValD_copy_rec⋅r⋅(ValN⋅n) = ValN⋅n"
(*<*)

lemma ValD_copy_rec_strict [simp]:
  "ValD_copy_rec⋅r⋅⊥ = ⊥"
  by fixrec_simp

abbreviation
  "ValD_copy ≡ fix⋅ValD_copy_rec"

lemma ValD_copy_strict [simp]:
  "ValD_copy⋅⊥ = ⊥"
  by (subst fix_eq) simp

lemma ValD_copy_ID [simp]:
  "ValD_copy = ID"
proof -
  { fix x :: ValD
    fix i :: nat
    have "ValD_take i⋅(ValD_copy⋅(ValD_take i⋅x)) = ValD_take i⋅x"
    proof (induct i arbitrary: x)
      case (Suc n) then show ?case
        by (cases x) (subst fix_eq, simp add: cfun_map_def)+
    qed simp }
  then have "∧x :: ValD. (⊔i. ValD_take i⋅(ValD_copy⋅(ValD_take i⋅x))) = (⊔i. ValD_take i⋅x)"
    by (blast intro: lub_eq)
  then show ?thesis by (simp add: lub_distribs ValD.lub_take cfun_eq_iff)
qed

(*>*)
text‹

  interpret the PCF constants in the obvious ways. ``Ill-typed'' uses
  these combinators are mapped to @{term "⊥"}.

 ›

definition cond :: "ValD → ValD → ValD → ValD" where
  "cond ≡ Λ i t e. case i of ValF⋅f → ⊥ | ValTT → t | ValFF → e | ValN⋅n → ⊥"

definition succ :: "ValD → ValD" where
  "succ ≡ Λ (ValN⋅n). ValN⋅(n + 1)"

definition pred :: "ValD → ValD" where
  "pred ≡ Λ (ValN⋅n). case n of 0 → ⊥ | Suc n → ValN⋅n"

definition isZero :: "ValD → ValD" where
  "isZero ≡ Λ (ValN⋅n). if n = 0 then ValTT else ValFF"

text‹

  model environments simply as continuous functions from variable
  to values.

 ›

type_synonym Var = "var"
type_synonym 'a Env = "Var → 'a"

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

definition env_ext :: "Var → 'a → 'a Env → 'a Env" where
  "env_ext ≡ Λ v x ρ v'. if v = v' then x else ρ⋅v'"
(*<*)

lemma env_ext_same: "env_ext⋅v⋅x⋅ρ⋅v = x"
  by (simp add: env_ext_def)

lemma env_ext_neq: "v ≠ v' ==> env_ext⋅v⋅x⋅ρ⋅v' = ρ⋅v'"
  by (simp add: env_ext_def)

lemmas env_ext_simps[simp] = env_ext_same env_ext_neq

(*>*)
text‹

  semantics is given by a function defined by primitive recursion
  the syntax.

 ›

type_synonym EnvD = "ValD Env"

primrec
  evalD :: "expr → EnvD → ValD"
where
  "evalD (Var v) = (Λ ρ. ρ⋅v)"
| "evalD (App f x) = (Λ ρ. appF⋅(evalD f⋅ρ)⋅(evalD x⋅ρ))"
| "evalD (AbsN v e) = (Λ ρ. ValF⋅(Λ x. evalD e⋅(env_ext⋅v⋅x⋅ρ)))"
| "evalD (AbsV v e) = (Λ ρ. ValF⋅(strictify⋅(Λ x. evalD e⋅(env_ext⋅v⋅x⋅ρ))))"
| "evalD (Diverge) = (Λ ρ. ⊥)"
| "evalD (Fix v e) = (Λ ρ. μ x. evalD e⋅(env_ext⋅v⋅x⋅ρ))"
| "evalD (tt) = (Λ ρ. ValTT)"
| "evalD (ff) = (Λ ρ. ValFF)"
| "evalD (Cond i t e) = (Λ ρ. cond⋅(evalD i⋅ρ)⋅(evalD t⋅ρ)⋅(evalD e⋅ρ))"
| "evalD (Num n) = (Λ ρ. ValN⋅n)"
| "evalD (Succ e) = (Λ ρ. succ⋅(evalD e⋅ρ))"
| "evalD (Pred e) = (Λ ρ. pred⋅(evalD e⋅ρ))"
| "evalD (IsZero e) = (Λ ρ. isZero⋅(evalD e⋅ρ))"

abbreviation eval' :: "expr → ValD Env → ValD" (‹[_]_› [0,1000] 60) where
  "eval' M ρ ≡ evalD M⋅ρ"


subsection‹The Y Combinator›

text‹

  can shown the Y combinator is the least fixed point operator using
  the minimal invariant. In other words, @{term "fix"} is
  in untyped PCF minus the @{term "Fix"} construct.

  is Example~3.6 from 🚫‹"PittsAM:relpod"›. He attributes the
  to Plotkin.

  two functions are ‹Δ ≡ λf x. f (x x)› and ‹Y ≡
 λf. (Δ f) (Δ f)›.

  the numbers here are names, not de Bruijn indices.

 ›

definition Y_delta :: expr where
  "Y_delta ≡ AbsN 0 (AbsN 1 (App (Var 0) (App (Var 1) (Var 1))))"

definition Ycomb :: expr where
  "Ycomb ≡ AbsN 0 (App (App Y_delta (Var 0)) (App Y_delta (Var 0)))"

definition fixD :: "ValD → ValD" where
  "fixD ≡ Λ (ValF⋅f). fix⋅f"

lemma Y: "[Ycomb]ρ = ValF⋅fixD"
(*<*)
proof(rule below_antisym)
  show "ValF⋅fixD ⊑ [Ycomb]ρ"
    unfolding fixD_def Ycomb_def
    apply (clarsimp simp: cfun_below_iff eta_cfun)
    apply (case_tac x)
     apply simp_all
    apply (rule fix_least)
    by (subst Y_delta_def, simp)
next
  { fix f ρ
    let ?P = "λx. x ⊑ ID ∧ appF⋅(x⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f)))⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f)) ⊑ fixD⋅(ValF⋅f)"
    have "?P ValD_copy"
      apply (rule fix_ind)
        apply simp
       apply simp
      apply clarsimp
      apply (rule conjI)
       apply (rule cfun_belowI)
       apply (case_tac xa)
        apply simp_all
       apply (drule cfun_map_below_ID)
       apply (simp add: cfun_below_iff)
      apply (simp add: fixD_def eta_cfun)
      apply (subst Y_delta_def)
      apply (subst fix_eq)
      apply simp
      apply (rule cfun_below_ID, assumption)
      apply (rule monofun_cfun_arg)
      apply (subgoal_tac "appF⋅(x⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f)))⋅(x⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f)))
                        ⊑ appF⋅(x⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f)))⋅(appF⋅([Y_delta]ρ)⋅(ValF⋅f))")
       apply (erule (1) below_trans)
      apply (simp add: monofun_cfun_arg cfun_below_iff)
      done }
  then show "[Ycomb]ρ ⊑ ValF⋅fixD"
    unfolding Ycomb_def fixD_def
    apply (clarsimp simp: cfun_below_iff)
    apply (case_tac x)
    apply (subst Y_delta_def, simp)
    apply simp
    apply (subst Y_delta_def, simp)+
    done
qed

(* FIXME could also try to show uniformity, cf Gunter, Plotkin "3 Inadequate Models". *)

(*>*)

subsection‹Logical relations for definability›

text‹

 label{sec:pcfdefinability}

  element of @{typ "ValD"} is definable if there is an expression
  denotes it.

 ›

definition definable :: "ValD → bool" where
  "definable d ≡ ∃M. [M]env_empty = d"

text‹

  classical result about PCF is that while the denotational semantics
  \emph{adequate}, as we show in \S\ref{sec:opsem}, it is not
 emph{fully abstract}, i.e. it contains undefinable values (junk).

  way of showing this is to reason operationally; see, for instance,
 🚫‹‹\S4› in "Plotkin77"› and 🚫‹‹\S6.1› in "Gunter:1992"›.

  is to use \emph{logical relations}, following
 🚫‹"Plotkin:1973"›, and also
 🚫‹"Mitchell:1996" and "Sieber:1992" and "DBLP:conf/mfps/Stoughton93"›.

  this purpose we define a logical relation to be a set of vectors
  @{typ "ValD"} that is closed under continuous functions of type
 {typ "ValD → ValD"}. This is complicated by the @{term "ValF"} tag
  having strict function abstraction.

 ›

definition
  logical_relation :: "('i::type → ValD) set → bool"
where
  "logical_relation R ≡
     (∀fs ∈ R. ∀xs ∈ R. (λj. appF⋅(fs j)⋅(xs j)) ∈ R)
   ∧ (∀fs ∈ R. ∀xs ∈ R. (λj. strictify⋅(appF⋅(fs j))⋅(xs j)) ∈ R)
   ∧ (∀fs. (∀xs ∈ R. (λj. (fs j)⋅(xs j)) ∈ R) ⟶ (λj. ValF⋅(fs j)) ∈ R)
   ∧ (∀fs. (∀xs ∈ R. (λj. strictify⋅(fs j)⋅(xs j)) ∈ R) ⟶ (λj. ValF⋅(strictify⋅(fs j))) ∈ R)
   ∧ (∀xs ∈ R. (λj. fixD⋅(xs j)) ∈ R)
   ∧ (∀cs ∈ R. ∀ts ∈ R. ∀es ∈ R. (λj. cond⋅(cs j)⋅(ts j)⋅(es j)) ∈ R)
   ∧ (∀xs ∈ R. (λj. succ⋅(xs j)) ∈ R)
   ∧ (∀xs ∈ R. (λj. pred⋅(xs j)) ∈ R)
   ∧ (∀xs ∈ R. (λj. isZero⋅(xs j)) ∈ R)"
(*<*)

lemma logical_relationI:
  "[ ∧fs xs. [ fs ∈ R; xs ∈ R ] ==> (λj. appF⋅(fs j)⋅(xs j)) ∈ R;
     ∧fs xs. [ fs ∈ R; xs ∈ R ] ==> (λj. strictify⋅(appF⋅(fs j))⋅(xs j)) ∈ R;
     ∧fs. (∧xs. xs ∈ R ==> (λj. (fs j)⋅(xs j)) ∈ R) ==> (λj. ValF⋅(fs j)) ∈ R;
     ∧fs. (∧xs. xs ∈ R ==> (λj. strictify⋅(fs j)⋅(xs j)) ∈ R) ==> (λj. ValF⋅(strictify⋅(fs j))) ∈ R;
     ∧xs. xs ∈ R ==> (λj. fixD⋅(xs j)) ∈ R;
     ∧cs ts es. [ cs ∈ R; ts ∈ R; es ∈ R ] ==> (λj. cond⋅(cs j)⋅(ts j)⋅(es j)) ∈ R;
     ∧xs. xs ∈ R ==> (λj. succ⋅(xs j)) ∈ R;
     ∧xs. xs ∈ R ==> (λj. pred⋅(xs j)) ∈ R;
     ∧xs. xs ∈ R ==> (λj. isZero⋅(xs j)) ∈ R ] ==> logical_relation R"
  unfolding logical_relation_def by (simp add: cfcomp1)

lemma lr_l2r:
  "[ fs ∈ R; xs ∈ R; logical_relation R ] ==> (λj. appF⋅(fs j)⋅(xs j)) ∈ R"
  "[ fs ∈ R; xs ∈ R; logical_relation R ] ==> (λj. strictify⋅(appF⋅(fs j))⋅(xs j)) ∈ R"
  "[ xs ∈ R; logical_relation R ] ==> (λj. fixD⋅(xs j)) ∈ R"
  "[ cs ∈ R; ts ∈ R; es ∈ R; logical_relation R ] ==> (λj. cond⋅(cs j)⋅(ts j)⋅(es j)) ∈ R"
  "[ xs ∈ R; logical_relation R ] ==> (λj. succ⋅(xs j)) ∈ R"
  "[ xs ∈ R; logical_relation R ] ==> (λj. pred⋅(xs j)) ∈ R"
  "[ xs ∈ R; logical_relation R ] ==> (λj. isZero⋅(xs j)) ∈ R"
  unfolding logical_relation_def by blast+

lemma lr_r2l:
  "[ logical_relation R; ∀xs ∈ R. (λj. (fs j)⋅(xs j)) ∈ R ] ==> (λi. ValF⋅(fs i)) ∈ R"
  unfolding logical_relation_def by (simp add: cfcomp1)

lemma lr_r2l_strict:
  "[ logical_relation R; ∀xs ∈ R. (λj. strictify⋅(fs j)⋅(xs j)) ∈ R ] ==> (λi. ValF⋅(strictify⋅(fs i))) ∈ R"
  unfolding logical_relation_def by (simp add: cfcomp1)

(*>*)
text‹

  the context of PCF these relations also need to respect the
 .

 ›

definition
  PCF_consts_rel :: "('i::type → ValD) set → bool"
where
  "PCF_consts_rel R ≡
       ⊥ ∈ R
     ∧ (λi. ValTT) ∈ R
     ∧ (λi. ValFF) ∈ R
     ∧ (∀n. (λi. ValN⋅n) ∈ R)"
(*<*)

lemma PCF_consts_rel_simps [simp, elim]:
  "PCF_consts_rel R ==> ⊥ ∈ R"
  "PCF_consts_rel R ==> (λi. ValTT) ∈ R"
  "PCF_consts_rel R ==> (λi. ValFF) ∈ R"
  "PCF_consts_rel R ==> (λi. ValN⋅n) ∈ R"
unfolding PCF_consts_rel_def by simp_all

lemma PCF_consts_relI:
  "[ ⊥ ∈ R;
     (λi. ValTT) ∈ R;
     (λi. ValFF) ∈ R;
     ∧n. (λi. ValN⋅n) ∈ R ] ==> PCF_consts_rel R"
unfolding PCF_consts_rel_def by blast

(*>*)
text‹›

abbreviation
  "PCF_lr R ≡ adm (λx. x ∈ R) ∧ logical_relation R ∧ PCF_consts_rel R"

text‹

  fundamental property of logical relations states that all PCF
  satisfy all PCF logical relations. This result is
  due to 🚫‹"Plotkin:1973"›. The proof is by a
  induction on the expression @{term "M"}.

 ›

lemma lr_fundamental:
  assumes lr: "PCF_lr R"
  assumes ρ: "∀v. (λi. ρ i⋅v) ∈ R"
  shows "(λi. [M](ρ i)) ∈ R"
(*<*)
using ρ
proof(induct M arbitrary: ρ)
  case (Var v ρ) then show ?case by simp
next
  case (App e1 e2 ρ)
  with lr lr_l2r(1)[where fs="λj. [e1](ρ j)" and xs="λj. [e2](ρ j)"]
  show ?case by simp
next
  case (AbsN v e)
  with lr show ?case
    apply clarsimp
    apply (erule lr_r2l[where fs="λi. Λ x. [e](env_ext⋅v⋅x⋅(ρ i))" and R=R, simplified])
    apply clarsimp
    apply (cut_tac ρ="λj. env_ext⋅v⋅(xs j)⋅(ρ j)" in AbsN.hyps)
     apply (simp add: env_ext_def)
     using AbsN(2)
     apply clarsimp
     apply (case_tac "v=va")
      apply (simp add: eta_cfun)
     apply simp
    apply simp
    done
next
  case (AbsV v e)
  with lr show ?case
    apply clarsimp
    apply (rule lr_r2l_strict[where fs="λi. Λ x. [e](env_ext⋅v⋅x⋅(ρ i))", simplified])
     apply simp
    apply clarsimp
    apply (cut_tac fs="λi. ValF⋅(Λ x. [e](env_ext⋅v⋅x⋅(ρ i)))" and xs=xs and R=R in lr_l2r(2))
     apply simp_all
    apply (erule lr_r2l[where fs="λi. Λ x. [e](env_ext⋅v⋅x⋅(ρ i))" and R=R, simplified])
    apply clarsimp
    apply (cut_tac ρ="λj. env_ext⋅v⋅(xsa j)⋅(ρ j)" in AbsV.hyps)
     apply (simp add: env_ext_def)
     using AbsV(2)
     apply clarsimp
     apply (case_tac "v=va")
      apply (simp add: eta_cfun)
     apply simp
    apply simp
    done
next
  case (Fix v e ρ) show ?case
    apply simp
    apply (subst fix_argument_promote_fun)
    apply (rule fix_ind[where F="Λ f. (λx. (Λ xa. [e](env_ext⋅v⋅xa⋅(ρ x)))⋅(f x))"])
      apply (simp add: lr)
     apply (simp add: lr inst_fun_pcpo[symmetric])
    apply simp
    apply (cut_tac ρ="λi. env_ext⋅v⋅(x i)⋅(ρ i)" in Fix.hyps)
     unfolding env_ext_def
     using Fix(2)
     apply clarsimp
     apply (case_tac "v=va")
      apply (simp add: eta_cfun)
     apply simp
    apply (simp add: cont_fun)
    done
next
  case (Cond i t e ρ)
  with lr lr_l2r(4)[where cs="λj. [i](ρ j)" and ts="λj. [t](ρ j)" and es="λj. [e](ρ j)"]
  show ?case by simp
next
  case (Succ e ρ)
  with lr lr_l2r(5)[where xs="λj. [e](ρ j)"]
  show ?case by simp
next
  case (Pred e ρ)
  with lr lr_l2r(6)[where xs="λj. [e](ρ j)"]
  show ?case by simp
next
  case (IsZero e ρ)
  with lr lr_l2r(7)[where xs="λj. [e](ρ j)"]
  show ?case by simp
next
  case Diverge with lr show ?case
    apply simp
    apply (simp add: inst_fun_pcpo[symmetric])
    done
qed (insert lr, simp_all)
(*>*)

text‹

  can use this result to show that there is no PCF term that maps the
  @{term "args ∈ R"} to @{term "result ∉ R"} for some logical
  @{term "R"}. If we further show that there is a function
 {term "f"} in @{term "ValD"} such that @{term "f args = result"} then
  can conclude that @{term "f"} is not definable.

 ›

abbreviation
  appFLv :: "ValD → ('i::type → ValD) list → ('i → ValD)"
where
  "appFLv f args ≡ (λi. foldl (λf x. appF⋅f⋅(x i)) f args)"

lemma lr_appFLv:
  assumes lr: "logical_relation R"
  assumes f: "(λi::'i::type. f) ∈ R"
  assumes args: "set args ⊆ R"
  shows "appFLv f args ∈ R"
(*<*)
using args
proof(induct args rule: rev_induct)
  case Nil with f show ?case by simp
next
  case (snoc x xs) then show ?case
    using lr_l2r(1)[OF _ _ lr, where fs="λi. (foldl (λf x. appF⋅f⋅(x i)) f xs)" and xs=x]
    by simp
qed

(*>*)
text‹›

corollary not_definable:
  fixes R :: "('i::type → ValD) set"
  fixes args :: "('i → ValD) list"
  fixes result :: "'i → ValD"
  assumes lr: "PCF_lr R"
  assumes args: "set args ⊆ R"
  assumes result: "result ∉ R"
  shows "¬(∃(f::ValD). definable f ∧ appFLv f args = result)"
(*<*)
proof
  assume "∃f. definable f ∧ appFLv f args = result"
  then obtain f
    where df: "definable f"
      and f: "appFLv f args = result" by blast
  from df obtain M
    where Mf: "[M]env_empty = f"
    unfolding definable_def by blast
  with lr lr_fundamental[OF lr, where M=M and ρ="λi. env_empty"]
       f args lr_appFLv[where f=f and R=R and args=args]
  have "result ∈ R" unfolding env_empty_def by (simp add: inst_fun_pcpo[symmetric])
  with result show False ..
qed
(*>*)

subsection‹Parallel OR is not definable›

text ‹

 label{sec:por}

  show that parallel-or is not ‹λ›-definable following
 🚫‹"Sieber:1992"› and 🚫‹"DBLP:conf/mfps/Stoughton93"›.

 -or is similar to the familiar short-circuting or except that
  the first argument is @{term "⊥"} and the second one is
 {term "ValTT"}, we get @{term "ValTT"} (and not @{term
 ⊥"}). It is continuous and then have included in the @{typ
 ValD"} domain.

 ›

definition por :: "ValD → ValD → ValD" (‹_ por _› [31,30] 30) where
  "x por y ≡
     if x = ValTT then ValTT
       else if y = ValTT then ValTT
              else if (x = ValFF ∧ y = ValFF) then ValFF else ⊥"

text‹The defining properties of parallel-or.›

lemma POR_simps [simp]:
  "(ValTT por y) = ValTT"
  "(x por ValTT) = ValTT"
  "(ValFF por ValFF) = ValFF"
  "(ValFF por ⊥) = ⊥"
  "(ValFF por ValN⋅n) = ⊥"
  "(ValFF por ValF⋅f) = ⊥"
  "(⊥ por ValFF) = ⊥"
  "(ValN⋅n por ValFF) = ⊥"
  "(ValF⋅f por ValFF) = ⊥"
  "(⊥ por ⊥) = ⊥"
  "(⊥ por ValN⋅n) = ⊥"
  "(⊥ por ValF⋅f) = ⊥"
  "(ValN⋅n por ⊥) = ⊥"
  "(ValF⋅f por ⊥) = ⊥"
  "(ValN⋅m por ValN⋅n) = ⊥"
  "(ValN⋅n por ValF⋅f) = ⊥"
  "(ValF⋅f por ValN⋅n) = ⊥"
  "(ValF⋅f por ValF⋅g) = ⊥"
  unfolding por_def by simp_all
(*<*)

text‹

  show that parallel-or is a continuous function.

 ›

lemma POR_sym: "(x por y) = (y por x)"
  unfolding por_def by simp

lemma ValTT_below_iff [simp]: "ValTT ⊑ x ⟷ x = ValTT"
  by (cases x) simp_all

lemma ValFF_below_iff [simp]: "ValFF ⊑ x ⟷ x = ValFF"
  by (cases x) simp_all

lemma monofun_por: "monofun (λx. x por y)"
  unfolding por_def
  by (rule monofunI) auto

lemma mic2mic: "max_in_chain i Y ==> max_in_chain i (λi. f (Y i))"
  unfolding max_in_chain_def by simp

lemma cont_por1: "cont (λx. x por y)"
  apply (rule contI2[OF monofun_por])
  apply (case_tac "Lub Y")
   apply simp_all
   apply (cases y)
   apply simp_all
   apply (cases y)
   apply simp_all

   apply (frule compact_imp_max_in_chain)
    apply simp
   apply clarsimp
   apply (frule mic2mic[where f="λx. x por y"])
   apply (subst iffD1[OF maxinch_is_thelub])
   apply simp_all
   apply (simp_all add: maxinch_is_thelub)

   apply (frule compact_imp_max_in_chain)
    apply simp
   apply clarsimp
   apply (frule mic2mic[where f="λx. x por y"])
   apply (subst iffD1[OF maxinch_is_thelub])
   apply simp_all
   apply (simp_all add: maxinch_is_thelub)

   apply (cases y)
   apply simp_all
   done

lemma cont_por[cont2cont, simp]:
  assumes f: "cont (λx. f x)" and g: "cont (λx. g x)"
  shows "cont (λx. f x por g x)"
proof -
  have A: "∧f y. cont f ==> cont (λx. f x por y)"
    by (rule cont_apply) (simp_all add: cont_por1)
  from A[OF f] A[OF g] show ?thesis
    by (auto simp: cont_por1 POR_sym intro: cont_apply[OF f])
qed

(*>*)
text‹

  need three-element vectors.

 ›

datatype Three = One | Two | Three

text‹

  standard logical relation @{term "R"} that demonstrates POR is not
  is:
 [
 (x, y, z) \in R\ \mbox{iff}\ x = y = z \lor (x = \bot \lor y = \bot)
 ]
  POR satisfies this relation can be seen from its truth table (see
 ).

  we restrict the ‹x = y = z› clause to non-function
 . Adding functions breaks the ``logical relations'' property.

 ›

definition
  POR_base_lf_rep :: "(Three → ValD) lf_rep"
where
  "POR_base_lf_rep ≡ λ(mR, pR).
     { (λi. ValTT) } ∪ { (λi. ValFF) } ― ‹‹x = y = z› for bools›
   ∪ (∪n. { (λi. ValN⋅n) }) ― ‹‹x = y = z› for numerals›
   ∪ { f . f One = ⊥ } ― ‹‹x = ⊥››
   ∪ { f . f Two = ⊥ } ― ‹‹y = ⊥››"

text‹

We close this relation with respect to continuous functions. This
functor yields an admissible relation for all @{term " "} and is
 .

 ›

definition
  fn_lf_rep :: "('i::type → ValD) lf_rep"
where
  "fn_lf_rep ≡ λ(mR, pR). { λi. ValF⋅(fs i) |fs. ∀xs ∈ unlr (undual mR). (λj. (fs j)⋅(xs j)) ∈ unlr pR }"
(*<*)

lemma adm_POR_base_lf_rep:
  "adm (λx. x ∈ POR_base_lf_rep r)"
unfolding POR_base_lf_rep_def
using adm_below_monic_exists[OF _ below_monic_fun_K[where f="ValN"], where P="λ_. True", simplified]
by (auto intro!: adm_disj simp: cont_fun)

lemma mono_POR_base_lf_rep:
  "mono POR_base_lf_rep"
unfolding POR_base_lf_rep_def by (blast intro!: monoI)

lemma adm_fn:
  shows "adm (λx. x ∈ fn_lf_rep r)"
unfolding fn_lf_rep_def
using adm_below_monic_exists[OF _ below_monic_fun_K[where f="ValF"], where P="λ_. True", simplified]
apply (clarsimp simp: split_def)
apply (rule adm_below_monic_exists)
apply (auto simp: cont_fun below_monic_indexed)
done

(*
  by (fastforce simp: split_def intro: adm_below_monic_exists)
*)

lemma mono_fn_lf_rep:
  "mono fn_lf_rep"
proof
  fix x y :: "('a → ValD) admS dual × ('a → ValD) admS"
  obtain x1 x2 y1 y2 where [simp]: "x = (x1, x2)" "y = (y1, y2)"
    by (cases x, cases y)
  assume "x ≤ y"
  then show "fn_lf_rep x ⊆ fn_lf_rep y"
    by (simp add: fn_lf_rep_def) (use dual_less_eq_iff less_eq_admS_def in blast)
qed

(*>*)
text‹›

definition POR_lf_rep :: "(Three → ValD) lf_rep" where
  "POR_lf_rep R ≡ POR_base_lf_rep R ∪ fn_lf_rep R"

abbreviation "POR_lf ≡ λr. mklr (POR_lf_rep r)"
(*<*)

lemma admS_POR_lf [intro, simp]:
  "POR_lf_rep r ∈ admS"
proof
  show "⊥ ∈ POR_lf_rep r"
    unfolding POR_lf_rep_def POR_base_lf_rep_def
    by simp
next
  show "adm (λx. x ∈ POR_lf_rep r)"
    unfolding POR_lf_rep_def
    using adm_POR_base_lf_rep[of r] adm_fn[of r] by simp
qed

lemma mono_POR_lf:
  "mono POR_lf"
  apply (rule monoI)
  apply simp
  unfolding POR_lf_rep_def
  using mono_fn_lf_rep mono_POR_base_lf_rep
  apply (blast dest: monoD)
  done

(*>*)
text‹

  it yields an admissible relation and is monotonic.

  need to show the functor respects the minimal invariant.

 ›

lemma min_inv_POR_lf:
  assumes "eRSV e R' S'"
  shows "eRSV (ValD_copy_rec⋅e) (dual (POR_lf (dual S', undual R'))) (POR_lf (R', S'))"
(*<*)
  apply clarsimp
  apply (simp add: POR_lf_rep_def)
  apply (elim disjE)
   apply (rule disjI1)
   apply (auto simp: POR_base_lf_rep_def eta_cfun cfcomp1 cfun_eq_iff)[1]
  apply (rule disjI2)
  using assms
  apply (clarsimp simp: fn_lf_rep_def eta_cfun)
  apply (simp add: cfcomp1 cfun_map_def)
  apply (rule_tac x="λi. Λ xa. e⋅(fs i⋅(e⋅xa))" in exI)
  apply force
  done

interpretation POR: DomSolV POR_lf ValD_copy_rec
  apply standard
    apply (rule mono_POR_lf)
   apply (rule ValD_copy_ID)
  apply (erule min_inv_POR_lf)
  done

lemma PORI [intro, simp]:
  "(λi. ValTT) ∈ unlr POR.delta"
  "(λi. ValFF) ∈ unlr POR.delta"
  "(λi. ValN⋅n) ∈ unlr POR.delta"
  "f One = ⊥ ==> f ∈ unlr POR.delta"
  "f Two = ⊥ ==> f ∈ unlr POR.delta"
  "[ ∧xs. xs ∈ unlr POR.delta ==> (λj. (fs j)⋅(xs j)) ∈ unlr POR.delta ] ==> (λi. ValF⋅(fs i)) ∈ unlr POR.delta"
  by (subst POR.delta_sol, simp, subst POR_lf_rep_def,
      fastforce simp: POR_base_lf_rep_def fn_lf_rep_def eta_cfun cfcomp1)+

lemma PORE:
  "[ a ∈ unlr POR.delta;
     (a = (λi. ValTT) ==> P);
     (a = (λi. ValFF) ==> P);
     (∧n. a = (λi. ValN⋅n) ==> P);
     (a One = ⊥ ==> P);
     (a Two = ⊥ ==> P);
     (∧fs. [ a = (λi. ValF⋅(fs i)); ∧xs. xs ∈ unlr POR.delta ==> (λj. (fs j)⋅(xs j)) ∈ unlr POR.delta ] ==> P)
   ] ==> P"
  apply (subst (asm) POR.delta_sol)
  apply simp
  apply (subst (asm) POR_lf_rep_def)
  apply (fastforce simp: POR_base_lf_rep_def fn_lf_rep_def eta_cfun)
  done

lemma POR_strict_appI:
  assumes "xs ∈ unlr POR.delta"
  assumes "∧xs. xs ∈ unlr POR.delta ==> (λj. fs j⋅(xs j)) ∈ unlr POR.delta"
  shows "(λj. strictify⋅(fs j)⋅(xs j)) ∈ unlr POR.delta"
using assms by - (erule PORE; simp)

lemma logical_relation_POR:
  "logical_relation (unlr POR.delta)"
  apply (rule logical_relationI)

  (* Strict application *)
  prefer 2
  apply (cut_tac fs="λi. appF⋅(fs i)" and xs=xs in POR_strict_appI)
   apply simp_all
  apply (auto elim: PORE)[1]

  (* FIXME fixD *)
  prefer 2
  apply (erule PORE)
  apply (simp_all add: fixD_def)
  apply (subst fix_argument_promote_fun)
  apply (rule_tac F="Λ f. (λx. fs x⋅(f x))" in fix_ind)
  apply (simp_all split: nat.split add: cont_fun)

  apply (auto elim: PORE simp: cond_def isZero_def pred_def succ_def eta_cfun split: nat.split)
  done

lemma PCF_consts_rel_POR:
  "PCF_consts_rel (unlr POR.delta)"
  by (rule PCF_consts_relI) simp_all

(*>*)
text‹

  can show that the solution satisfies the expectations of the
  theorem @{thm [source] "lr_fundamental"}.

 ›

lemma PCF_lr_POR_delta: "PCF_lr (unlr POR.delta)"
(*<*)
  using logical_relation_POR PCF_consts_rel_POR by fastforce
(*>*)
text‹

  is the truth-table for POR rendered as a vector: we seek a
  that simultaneously maps the two argument vectors to the
 .

 ›

definition POR_arg1_rel where
  "POR_arg1_rel ≡ λi. case i of One → ValTT | Two → ⊥ | Three → ValFF"

definition POR_arg2_rel where
  "POR_arg2_rel ≡ λi. case i of One → ⊥ | Two → ValTT | Three → ValFF"

definition POR_result_rel where
  "POR_result_rel ≡ λi. case i of One → ValTT | Two → ValTT | Three → ValFF"

lemma lr_POR_arg1_rel: "POR_arg1_rel ∈ unlr POR.delta"
  unfolding POR_arg1_rel_def by auto

lemma lr_POR_arg2_rel: "POR_arg2_rel ∈ unlr POR.delta"
  unfolding POR_arg2_rel_def by auto

lemma lr_POR_result_rel: "POR_result_rel ∉ unlr POR.delta"
(*<*)
  unfolding POR_result_rel_def
  apply clarify
  apply (erule PORE)
  apply (auto iff: fun_eq_iff split: Three.splits)
  done

(*>*)
text‹

 -or satisfies these tests:

 ›

theorem POR_sat:
  "appFLv (ValF⋅(Λ x. ValF⋅(Λ y. x por y))) [POR_arg1_rel, POR_arg2_rel] = POR_result_rel"
  unfolding POR_arg1_rel_def POR_arg2_rel_def POR_result_rel_def
  by (simp add: fun_eq_iff split: Three.splits)

text‹

 .. but is not PCF-definable:

 ›

theorem POR_is_not_definable:
  shows "¬(∃f. definable f ∧ appFLv f [POR_arg1_rel, POR_arg2_rel] = POR_result_rel)"
  apply (rule not_definable[where R="unlr POR.delta"])
    using lr_POR_arg1_rel lr_POR_arg2_rel lr_POR_result_rel PCF_lr_POR_delta
    apply simp_all
  done


subsection‹Plotkin's existential quantifier›

text‹

  can also show that the existential quantifier of
 🚫‹‹\S5› in "Plotkin77"› is not PCF-definable using logical relations.

  definition is quite loose; if the argument function @{term "f"}
  any value to @{term "ValTT"} then @{term "plotkin_exists"} yields
 {term "ValTT"}. It may be more plausible to test @{term "f"} on
  only.

 ›

definition plotkin_exists :: "ValD → ValD" where
  "plotkin_exists f ≡
     if (appF⋅f⋅⊥ = ValFF)
       then ValFF
       else if (∃n. appF⋅f⋅n = ValTT) then ValTT else ⊥"
(*<*)

lemma plotkin_exists_simps [simp]:
  "plotkin_exists ⊥ = ⊥"
  "plotkin_exists (ValF⋅⊥) = ⊥"
  "plotkin_exists (ValF⋅(Λ _. ValFF)) = ValFF"
  unfolding plotkin_exists_def by simp_all

lemma plotkin_exists_tt [simp]:
  "appF⋅f⋅(ValN⋅n) = ValTT ==> plotkin_exists f = ValTT"
  unfolding plotkin_exists_def
  using monofun_cfun_arg[where f="appF⋅f" and x="⊥"]
  by auto

lemma monofun_pe:
  "monofun plotkin_exists"
proof(rule monofunI)
  fix f g assume fg: "(f::ValD) ⊑ g"
  let ?goal = "plotkin_exists f ⊑ plotkin_exists g"
  {
    assume fbot: "appF⋅f⋅⊥ = ValFF"
    with fg have "appF⋅g⋅⊥ = ValFF"
      using monofun_cfun[where f="appF⋅f" and g="appF⋅g" and x="⊥"]
      by (simp add: monofun_cfun_arg)
    with fbot have ?goal by (simp add: plotkin_exists_def)
  }
  moreover
  {
    assume efn: "∃n. appF⋅f⋅n = ValTT"
    then obtain n where fn: "appF⋅f⋅n = ValTT" by blast
    then have fbot: "appF⋅f⋅⊥ ≠ ValFF"
      using monofun_cfun_arg[where f="appF⋅f" and x="⊥" and y="n"] by fastforce
    from fg have "appF⋅f⋅n ⊑ appF⋅g⋅n"
      using monofun_cfun_arg[OF fg, where f=appF]
      by (simp only: cfun_below_iff)
    with fn have gn: "appF⋅g⋅n = ValTT"
      using ValD.nchotomy[where y="appF⋅g⋅⊥"] by simp
    then have gbot: "appF⋅g⋅⊥ ≠ ValFF"
      using monofun_cfun_arg[where f="appF⋅g" and x="⊥" and y="n"] by fastforce
    from fn gn fbot gbot have ?goal apply (unfold plotkin_exists_def) by fastforce
  }
  moreover
  {
    assume fbot: "appF⋅f⋅⊥ ≠ ValFF" and efn: "¬(∃n. appF⋅f⋅n = ValTT)"
    then have ?goal by (simp add: plotkin_exists_def)
  }
  ultimately show ?goal unfolding plotkin_exists_def by blast
qed

(*>*)
text‹

  can show this function is continuous.

 ›

lemma cont_pe [cont2cont, simp]: "cont plotkin_exists"
(*<*)
proof (rule contI2[OF monofun_pe])
  fix Y assume Y: "chain (Y :: nat → ValD)"
  let ?goal = "plotkin_exists (⊔ i. Y i) ⊑ (⊔ i. plotkin_exists (Y i))"
  have peY: "chain (λi. plotkin_exists (Y i))"
    by (rule chainI, simp add: monofunE[OF monofun_pe] chainE[OF Y])
  {
    assume "∃i. appF⋅(Y i)⋅⊥ = ValFF"
    then obtain i where Yi: "appF⋅(Y i)⋅⊥ = ValFF" by blast
    have "Y i ⊑ (⊔ i. Y i)"
      using is_ub_thelub[OF Y, where x=i] by simp
    then have "appF⋅(Y i)⋅⊥ ⊑ appF⋅(⊔ i. Y i)⋅⊥" by (fastforce intro: monofun_cfun)
    with Yi have "ValFF ⊑ appF⋅(⊔ i. Y i)⋅⊥" by simp
    then have "appF⋅(⊔ i. Y i)⋅⊥ = ValFF" using ValD.nchotomy[where y="appF⋅(⊔ i. Y i)⋅⊥"] by simp
    moreover
    from Yi have "plotkin_exists (Y i) = ValFF" by (simp add: plotkin_exists_def)
    then have "ValFF ⊑ (⊔ i. plotkin_exists (Y i))" using is_ub_thelub[OF peY, where x=i] by simp
    then have "ValFF = (⊔ i. plotkin_exists (Y i))" using ValD.nchotomy[where y="⊔ i. plotkin_exists (Y i)"] by simp
    ultimately have ?goal by (simp add: plotkin_exists_def)
  }
  moreover
  {
    assume "∃i j. appF⋅(Y i)⋅j = ValTT"
    then obtain i j where Yij: "appF⋅(Y i)⋅j = ValTT" by blast
    from Yij have Yib: "appF⋅(Y i)⋅⊥ ≠ ValFF"
      using monofun_cfun_arg[where f="appF⋅(Y i)" and x="⊥" and y=j] by clarsimp
    moreover
    from Yij have "appF⋅(Y i)⋅j ⊑ appF⋅(⊔ i. Y i)⋅j"
      using is_ub_thelub[OF Y, where x=i] by (fastforce intro: monofun_cfun)
    with Yij have Yjlub: "appF⋅(⊔ i. Y i)⋅j = ValTT"
      using ValD.nchotomy[where y="appF⋅(⊔ i. Y i)⋅j"] by simp
    moreover
    from Yjlub have "appF⋅(⊔ i. Y i)⋅⊥ ≠ ValFF"
      using monofun_cfun_arg[where f="appF⋅(⊔ i. Y i)" and x="⊥" and y=j] by auto
    moreover
    from Yib Yij have "plotkin_exists (Y i) = ValTT" by (auto simp add: plotkin_exists_def)
    then have "ValTT ⊑ (⊔ i. plotkin_exists (Y i))" using is_ub_thelub[OF peY, where x=i] by simp
    then have "ValTT = (⊔ i. plotkin_exists (Y i))" using ValD.nchotomy[where y="⊔ i. plotkin_exists (Y i)"] by simp
    ultimately have ?goal by (simp add: plotkin_exists_def)
  }
  moreover
  {
    assume nFF: "¬(∃i. appF⋅(Y i)⋅⊥ = ValFF)" and nTT: "¬(∃i j. appF⋅(Y i)⋅j = ValTT)"
    with Y have ?goal
      unfolding plotkin_exists_def
      using compact_below_lub_iff[OF ValD.compacts(2)]
            compact_below_lub_iff[OF ValD.compacts(3)]
      by (simp add: contlub_cfun_arg contlub_cfun_fun)
  }
  ultimately show ?goal by blast
qed

lemma cont_pe2[cont2cont, simp]: "cont f ==> cont (λx. plotkin_exists (f x))"
  by (rule cont_apply) simp_all

(*>*)
text‹

  we construct argument and result test vectors such that @{term
 plotkin_exists"} satisfies these tests but no PCF-definable term
 .

 ›

definition PE_arg_rel where
  "PE_arg_rel ≡ λi. ValF⋅(case i of
        0 → (Λ _. ValFF)
      | Suc n → (Λ (ValN⋅x). if x = Suc n then ValTT else ⊥))"

definition PE_result_rel where
  "PE_result_rel ≡ λi. case i of 0 → ValFF | Suc n → ValTT"

text‹

  that unlike the POR case the argument relation does not
  PE: we don't treat functions that return @{term "ValTT"}s
  @{term "ValFF"}s.

  Plotkin existential satisfies these tests:

 ›

theorem pe_sat:
  "appFLv (ValF⋅(Λ x. plotkin_exists x)) [PE_arg_rel] = PE_result_rel"
  unfolding PE_arg_rel_def PE_result_rel_def
  by (clarsimp simp: fun_eq_iff split: nat.splits)

text‹

  for POR, the difference between the two vectors is that the
  can diverge but not the result.

 ›

definition PE_base_lf_rep :: "(nat → ValD) lf_rep" where
  "PE_base_lf_rep ≡ λ(mR, pR).
     { ⊥ }
   ∪ { (λi. ValTT) } ∪ { (λi. ValFF) } ― ‹‹x = y = z› for bools›
   ∪ (∪n. { (λi. ValN⋅n) }) ― ‹‹x = y = z› for numerals›
   ∪ { f . f 1 = ⊥ ∨ f 2 = ⊥ } ― ‹Vectors that diverge on one or two.›"
(*<*)

lemma adm_PE_base_lf_rep:
  "adm (λx. x ∈ PE_base_lf_rep r)"
unfolding PE_base_lf_rep_def
using adm_below_monic_exists[OF _ below_monic_fun_K[where f=ValN], where P="λ_. True"]
by (auto intro!: adm_disj simp: cont_fun)

lemma mono_PE_base_lf_rep:
  "mono PE_base_lf_rep"
unfolding PE_base_lf_rep_def
by (blast intro!: monoI)

(*>*)
text‹

Again we close this under the function space, and show that it is
admissible, monotonic and respects the minimal invariant.

\<close>

definition PE_lf_rep :: " nat → ValD) lf_rep" where
 "PE_lf_rep R ≡ PE_base_lf_rep R ∪ fn_lf_rep R"

  "PE_lf ≡ λr. mklr (PE_lf_rep r)"
(*<*)

lemma admS_PE_lf [intro, simp]:
  "PE_lf_rep r ∈ admS"
proof
  show "⊥ ∈ PE_lf_rep r"
    unfolding PE_lf_rep_def PE_base_lf_rep_def
    by simp
next
  show "adm (λx. x ∈ PE_lf_rep r)"
    unfolding PE_lf_rep_def
    using adm_PE_base_lf_rep[of r] adm_fn[of r] by simp
qed

lemma mono_PE_lf:
  "mono PE_lf"
  apply (rule monoI)
  apply simp
  unfolding PE_lf_rep_def
  using mono_fn_lf_rep mono_PE_base_lf_rep
  apply (blast dest: monoD)
  done

lemma min_inv_PE_lf:
  assumes "eRSV e R' S'"
  shows "eRSV (ValD_copy_rec⋅e) (dual (PE_lf (dual S', undual R'))) (PE_lf (R', S'))"
  apply clarsimp
  apply (simp add: PE_lf_rep_def)
  apply (elim disjE)
   apply (rule disjI1)
   apply (auto simp: PE_base_lf_rep_def eta_cfun cfcomp1 cfun_eq_iff)[1]
  apply (rule disjI2)
  using assms
  apply (clarsimp simp: fn_lf_rep_def eta_cfun)
  apply (simp add: cfcomp1 cfun_map_def)
  apply (rule_tac x="λx. Λ xa. e⋅(fs x⋅(e⋅xa))" in exI)
  apply force
  done

interpretation PE: DomSolV PE_lf ValD_copy_rec
  apply standard
    apply (rule mono_PE_lf)
   apply (rule ValD_copy_ID)
  apply (erule min_inv_PE_lf)
  done

lemma PEI [intro, simp]:
  "⊥ ∈ unlr PE.delta"
  "(λi. ValTT) ∈ unlr PE.delta"
  "(λi. ValFF) ∈ unlr PE.delta"
  "(λi. ValN⋅n) ∈ unlr PE.delta"
  "f 1 = ⊥ ==> f ∈ unlr PE.delta"
  "f 2 = ⊥ ==> f ∈ unlr PE.delta"
  "[ ∧xs. xs ∈ unlr PE.delta ==> (λj. (fs j)⋅(xs j)) ∈ unlr PE.delta ] ==> (λi. ValF⋅(fs i)) ∈ unlr PE.delta"
  by (subst PE.delta_sol, simp, subst PE_lf_rep_def,
      fastforce simp: PE_base_lf_rep_def fn_lf_rep_def eta_cfun cfcomp1)+

lemma PE_fun_constI:
  "[ ∧xs. xs ∈ unlr PE.delta ==> (λj. f⋅(xs j)) ∈ unlr PE.delta ] ==> (λi. ValF⋅f) ∈ unlr PE.delta"
  using PEI(7)[where fs="λ_. f"] by simp

lemma PEE:
  "[ a ∈ unlr PE.delta;
     (a = ⊥ ==> P);
     (a = (λi. ValTT) ==> P);
     (a = (λi. ValFF) ==> P);
     (∧n. a = (λi. ValN⋅n) ==> P);
     (a 1 = ⊥ ==> P);
     (a 2 = ⊥ ==> P);
     (∧fs. [ a = (λj. ValF⋅(fs j)); ∧xs. xs ∈ unlr PE.delta ==> (λj. (fs j)⋅(xs j)) ∈ unlr PE.delta ] ==> P)
   ] ==> P"
  apply (subst (asm) PE.delta_sol)
  apply simp
  apply (subst (asm) PE_lf_rep_def)
  apply (fastforce simp: PE_base_lf_rep_def fn_lf_rep_def eta_cfun)
  done

lemma PEE_strict_appI:
  assumes "xs ∈ unlr PE.delta"
  assumes "∧xs. xs ∈ unlr PE.delta ==> (λj. fs j⋅(xs j)) ∈ unlr PE.delta"
  shows "(λj. strictify⋅(fs j)⋅(xs j)) ∈ unlr PE.delta"
  using assms
  apply -
  apply (erule PEE)
  apply simp_all
  done

lemma logical_relation_PE:
  "logical_relation (unlr PE.delta)"
apply (rule logical_relationI)

  (* Strict application *)
  prefer 2
  apply (cut_tac fs="λi. appF⋅(fs i)" and xs=xs in PEE_strict_appI)
   apply simp_all
  apply (auto elim: PEE)[1]

  (* FIXME fixD *)
  prefer 2
  apply (erule PEE)
  apply (simp_all add: fixD_def)
  apply (subst fix_argument_promote_fun)
  apply (rule_tac F="Λ f. (λx. fs x⋅(f x))" in fix_ind)
  apply (simp_all split: nat.split add: cont_fun)

  apply (auto elim: PEE simp: cond_def isZero_def pred_def succ_def eta_cfun split: nat.split)
  done

lemma PCF_consts_rel_PE:
  "PCF_consts_rel (unlr PE.delta)"
  by (rule PCF_consts_relI) simp_all
(*>*)
text‹

  solution satisfies the expectations of the fundamental theorem:

 ›

lemma PCF_lr_PE_delta: "PCF_lr (unlr PE.delta)"
(*<*)
  using logical_relation_PE PCF_consts_rel_PE by fastforce
(*>*)

lemma lr_PE_arg_rel: "PE_arg_rel ∈ unlr PE.delta"
(*<*)
  unfolding PE_arg_rel_def
  apply (rule PEI(7))
  apply (erule PEE)
   apply simp_all
  apply (case_tac n)
   apply simp
  apply (case_tac nat)
   apply simp_all
  done
(*>*)

lemma lr_PE_result_rel: "PE_result_rel ∉ unlr PE.delta"
(*<*)
unfolding PE_result_rel_def
apply clarify
apply (erule PEE)
apply (auto iff: fun_eq_iff split: nat.splits)
done
(*>*)

theorem PE_is_not_definable: "¬(∃f. definable f ∧ appFLv f [PE_arg_rel] = PE_result_rel)"
(*<*)
apply (rule not_definable[where R="unlr PE.delta"])
  using lr_PE_arg_rel lr_PE_result_rel PCF_lr_PE_delta
  apply simp_all
done
(*>*)

subsection‹Concluding remarks›

text‹

  techniques could be used to show that Haskell's ‹seq›
  is not PCF-definable. (It is definable for each base
 `type'' separately, and requires some care on function values.) If we
  an (unlifted) product type then it should be provable that
  evaluation is required to support ‹seq› on these
  (given ‹seq› on all other objects). (See
 🚫‹‹\S5.4› in "DBLP:conf/hopl/HudakHJW07"› and sundry posts to the
  by Lennart Augustsson.) This may be difficult to do plausibly
  adding a type system.

 ›

(*<*)

end
(*>*)