Theory AbsCFCorrect

section ‹The abstract semantics is correct›

theory AbsCFCorrect
  imports AbsCF ExCF "HOL-Library.Adhoc_Overloading"
begin

default_sort type

text ‹
The intention of the abstract semantics is to safely approximate the real control flow. This means that every call recorded by the exact semantics must occur in the result provided by the abstract semantics, which in turn is allowed to predict more calls than actually done.
›

subsection ‹Abstraction functions›

text ‹
This relation is expressed by abstraction functions and approximation relations. For each of our data types, there is an abstraction function ‹abs_<type>›, mapping the a value from the exact setup to the corresponding value in the abstract view. The approximation relation then expresses the fact that one abstract value of such a type is safely approximated by another.

Because we need an abstraction function for contours, we extend the ‹contour› type class by the abstraction functions and two equations involving the ‹nb› and ‹\<binit>› symbols.
›

class contour_a = contour +
  fixes abs_cnt :: "contour ⇒ 'a"
  assumes abs_cnt_nb[simp]: "abs_cnt (nb b lab) = \<anb> (abs_cnt b) lab"
     and abs_cnt_initial[simp]: "abs_cnt(\<binit>) = \<abinit>"

instantiation unit :: contour_a
begin
definition "abs_cnt _ = ()"
instance by standard auto
end

text ‹
It would be unwieldly to always write out ‹abs_<type> x›. We would rather like to write ‹|x|› if the type of ‹x› is known, as Shivers does it as well. Isabelle allows one to use the same syntax for different symbols. In that case, it generates more than one parse tree and picks the (hopefully unique) tree that typechecks.

Unfortunately, this does not work well in our case: There are eight ‹abs_<type>› functions and some expressions later have multiple occurrences of these, causing an exponential blow-up of combinations.

Therefore, we use a module by Christian Sternagel and Alexander Krauss for ad-hoc overloading, where the choice of the concrete function is done at parse time and immediately. This is used in the following to set up the the symbol ‹|_|› for the family of abstraction functions.
›

consts abs :: "'a ⇒ 'b" (‹|_|›)

adhoc_overloading
  abs abs_cnt

definition abs_benv :: "benv ⇒ 'c::contour_a \<abenv>"
  where "abs_benv β = map_option abs_cnt ∘ β"

adhoc_overloading
  abs abs_benv

primrec abs_closure :: "closure ⇒ 'c::contour_a \<aclosure>"
  where "abs_closure (l,β) = (l,|β| )"

adhoc_overloading
  abs abs_closure

primrec abs_d :: "d ⇒ 'c::contour_a \<ad>"
  where "abs_d (DI i) = {}"
      | "abs_d (DP p) = {PP p}"
      | "abs_d (DC cl) = {PC |cl|}"
      | "abs_d (Stop) = {AStop}"

adhoc_overloading
  abs abs_d  

definition abs_venv :: "venv ⇒ 'c::contour_a \<avenv>"
  where "abs_venv ve = (λ(v,b_a). ⋃{(case ve (v,b) of Some d ⇒ |d| | None ⇒ {}) | b. |b| = b_a })"

adhoc_overloading
  abs abs_venv

definition abs_ccache :: "ccache ⇒ 'c::contour_a \<accache>"
  where "abs_ccache cc = (⋃((c,β),d) ∈ cc . {((c,abs_benv β), p) | p . p∈abs_d d})"
(* equivalent, but I already have cont2cont for UNION
  where "abs_ccache cc = { ((c,abs_benv β),p) | c β p d . ((c,β),d) ∈ cc ∧ p ∈ abs_d d}" *)

adhoc_overloading
  abs abs_ccache

fun abs_fstate :: "fstate ⇒ 'c::contour_a \<afstate>"
  where "abs_fstate (d,ds,ve,b) = (the_elem |d|, map abs_d ds, |ve|, |b| )"

adhoc_overloading
  abs abs_fstate

fun abs_cstate :: "cstate ⇒ 'c::contour_a \<acstate>"
  where "abs_cstate (c,β,ve,b) = (c, |β|, |ve|, |b| )"

adhoc_overloading
  abs abs_cstate

subsection ‹Lemmas about abstraction functions›

text ‹
Some results about the abstractions functions.
›

lemma abs_benv_empty[simp]: "|Map.empty| = Map.empty"
unfolding abs_benv_def by simp

lemma abs_benv_upd[simp]: "|β(c↦b)| = |β| (c ↦ |b| )"
  unfolding abs_benv_def by simp

lemma the_elem_is_Proc:
  assumes "isProc cnt"
  shows "the_elem |cnt| ∈ |cnt|"
using assms by (cases cnt)auto

lemma [simp]: "|{}| = {}" unfolding abs_ccache_def by auto

lemma abs_cache_singleton [simp]: "|{((c,β),d)}| = {((c, |β| ), p) |p. p ∈ |d|}"
  unfolding abs_ccache_def by simp

lemma abs_venv_empty[simp]: "|Map.empty| = {}."
  apply (rule ext) by (auto simp add: abs_venv_def smap_empty_def)


subsection ‹Approximation relation›

text ‹
The family of relations defined here capture the notion of safe approximation.
›

consts approx :: "'a ⇒ 'a ⇒ bool" (‹_ ⪅ _›)

definition venv_approx :: "'c \<avenv> ⇒'c \<avenv> ⇒ bool"
  where "venv_approx = smap_less"

adhoc_overloading
  approx venv_approx

definition ccache_approx :: "'c \<accache> ⇒'c \<accache> ⇒ bool"
  where "ccache_approx = less_eq"

adhoc_overloading
  approx ccache_approx

definition d_approx :: "'c \<ad> ⇒'c \<ad> ⇒ bool"
  where "d_approx = less_eq"

adhoc_overloading
  approx d_approx

definition ds_approx :: "'c \<ad> list ⇒'c \<ad> list ⇒ bool"
  where "ds_approx = list_all2 d_approx"

adhoc_overloading
  approx ds_approx

inductive fstate_approx :: "'c \<afstate> ⇒'c \<afstate> ⇒ bool"
  where "⟦ ve ⪅ ve' ; ds ⪅ ds' ⟧
         ⟹ fstate_approx (proc,ds,ve,b) (proc,ds',ve',b)"

adhoc_overloading
  approx fstate_approx

inductive cstate_approx :: "'c \<acstate> ⇒'c \<acstate> ⇒ bool"
  where "⟦ ve ⪅ ve' ⟧ ⟹ cstate_approx (c,β,ve,b) (c,β,ve',b)"

adhoc_overloading
  approx cstate_approx

subsection ‹Lemmas about the approximation relation›

text ‹
Most of the following lemmas reduce an approximation statement about larger structures, as they are occurring the semantics functions, to statements about the components.
›

lemma venv_approx_trans[trans]:
  fixes ve1 ve2 ve3 :: "'c \<avenv>"
  shows "⟦ ve1 ⪅ ve2; ve2 ⪅ ve3 ⟧ ⟹ (ve1 ⪅ ve3)"
  unfolding venv_approx_def by (rule smap_less_trans)

lemma abs_venv_union: "|ve1 ++ ve2| ⪅ |ve1| ∪. |ve2|"
  by (auto simp add: venv_approx_def smap_less_def abs_venv_def smap_union_def, split option.split_asm, auto)

lemma abs_venv_map_of_rev: "|map_of (rev l)| ⪅ ⋃. (map (λ(v,k). |[v ↦ k]| ) l)"
proof (induct l)
  case Nil show ?case unfolding abs_venv_def by (auto simp: venv_approx_def smap_less_def ) next
  case (Cons a l)
    obtain v k where "a=(v,k)" by (rule prod.exhaust)
    hence "|map_of (rev (a#l))| ⪅ ( |[v ↦ k]| ∪. |map_of (rev l)| ):: 'a \<avenv>"
      by (auto intro: abs_venv_union)
    also
    have "… ⪅ |[v ↦ k]| ∪. (⋃. (map (λ(v,k). |[v  ↦ k]| ) l))"
      by (auto intro!:smap_union_mono[OF smap_less_refl Cons[unfolded venv_approx_def]] simp:venv_approx_def)
    also
    have "… = ⋃. ( |[v ↦ k]| # map (λ(v,k). |[v ↦ k]| ) l)"
      by (rule smap_Union_union)
    also
    have "… = ⋃. (map (λ(v,k). |[v ↦ k]| ) (a#l))"
      using ‹a = (v,k)›
      by auto
    finally
    show ?case .
qed

lemma abs_venv_map_of: "|map_of l| ⪅ ⋃. (map (λ(v,k). |[v ↦ k]| ) l)"
  using abs_venv_map_of_rev[of "rev l"] by simp

lemma abs_venv_singleton: "|[(v,b) ↦ d]| = {(v,|b| ) := |d|}."
  by (rule ext, auto simp add:abs_venv_def smap_singleton_def smap_empty_def)

lemma ccache_approx_empty[simp]:
  fixes x :: "'c \<accache>"
  shows "{} ⪅ x"
  unfolding ccache_approx_def by simp

lemmas ccache_approx_trans[trans] = subset_trans[where 'a = "((label × 'c \<abenv>) × 'c \<aproc>)", folded ccache_approx_def]
lemmas Un_mono_approx = Un_mono[where 'a = "((label × 'c \<abenv>) × 'c \<aproc>)", folded ccache_approx_def]
lemmas Un_upper1_approx = Un_upper1[where 'a = "((label × 'c \<abenv>) × 'c \<aproc>)", folded ccache_approx_def]
lemmas Un_upper2_approx = Un_upper2[where 'a = "((label × 'c \<abenv>) × 'c \<aproc>)", folded ccache_approx_def]

lemma abs_ccache_union: "|c1 ∪ c2| ⪅ |c1| ∪ |c2|"
  unfolding ccache_approx_def abs_ccache_def by auto

lemma d_approx_empty[simp]: "{} ⪅ (d::'c \<ad>)"
  unfolding d_approx_def by simp

lemma ds_approx_empty[simp]: "[] ⪅ []"
  unfolding ds_approx_def by simp

subsection ‹Lemma 7›

text ‹
Shivers' lemma 7 says that ‹\<aA>› safely approximates ‹𝒜›.
›

lemma lemma7:
  assumes "|ve::venv| ⪅ ve_a"
  shows "|𝒜 f β ve| ⪅ \<aA> f |β| ve_a"
proof(cases f)
case (R _ v)
  from assms have assm': "⋀v b. case_option {} abs_d (ve (v,b)) ⪅ ve_a (v,|b| )"
    by (auto simp add:d_approx_def abs_venv_def venv_approx_def smap_less_def elim!:allE)
  show ?thesis
    proof(cases "β (binder v)")
    case None thus ?thesis using R by auto next
    case (Some b)
      thus ?thesis using R assm'[of v b]
         by (auto simp add:abs_benv_def split:option.split)
  qed
qed (auto simp add:d_approx_def)


subsection ‹Lemmas 8 and 9›

text ‹
The main goal of this section is to show that ‹\<aF>› safely approximates ‹ℱ› and that ‹\<aC>› safely approximates ‹𝒞›. This has to be shown at once, as the functions are mutually recursive and requires a fixed point induction. To that end, we have to augment the set of continuity lemmas.
›

lemma cont2cont_abs_ccache[cont2cont,simp]:
  assumes "cont f"
  shows "cont (λx. abs_ccache(f x))"
unfolding abs_ccache_def
using assms
by (rule cont2cont)(rule cont_const)

text ‹
Shivers proves these lemmas using parallel fixed point induction over the two fixed points (the one from the exact semantics and the one from the abstract semantics). But it is simpler and equivalent to just do induction over the exact semantics and keep the abstract semantics functions fixed, so this is what I am doing.
›


lemma lemma89:
 fixes fstate_a :: "'c::contour_a \<afstate>" and cstate_a :: "'c::contour_a \<acstate>"
 shows "|fstate| ⪅ fstate_a ⟹ |ℱ⋅(Discr fstate)| ⪅ \<aF>⋅(Discr fstate_a)"
   and "|cstate| ⪅ cstate_a ⟹ |𝒞⋅(Discr cstate)| ⪅ \<aC>⋅(Discr cstate_a)"
proof(induct arbitrary: fstate fstate_a cstate cstate_a rule: evalF_evalC_induct)
case Admissibility show ?case
  unfolding ccache_approx_def 
  by (intro adm_lemmas adm_subset adm_prod_split adm_not_conj adm_not_mem adm_single_valued cont2cont)
next
case Bottom {
  case 1 show ?case by simp next
  case 2 show ?case by simp next
}
next
case (Next evalF evalC) {
case 1
  obtain d ds ve b where fstate: "fstate = (d,ds,ve,b)"
    by (cases fstate, auto)
  moreover
  obtain proc ds_a ve_a b_a where fstate_a: "fstate_a = (proc,ds_a,ve_a,b_a)"
    by (cases fstate_a, auto)
  ultimately
  have abs_d: "the_elem |d| = proc"
   and abs_ds: "map abs_d ds ⪅ ds_a"
   and abs_ve: "|ve| ⪅ ve_a"
   and abs_b: "|b| = b_a"
  using 1 by (auto elim:fstate_approx.cases)

  from abs_ds have dslength: "length ds = length ds_a"
    by (auto simp add:ds_approx_def dest!:list_all2_lengthD)

  from fstate fstate_a abs_d abs_ds abs_ve abs_ds dslength
  show ?case
  proof(cases fstate rule:fstate_case, auto simp del:a_evalF.simps a_evalC.simps set_map)

  txt ‹Case Lambda›
  fix β and lab and vs:: "var list" and c
  assume ds_a_length: "length vs = length ds_a"

  have "|β(lab ↦ b)| = |β| (lab ↦ b_a)"
    unfolding below_fun_def using abs_b by simp
  moreover

  { have "|ve(map (λv. (v, b)) vs [↦] ds)|
          ⪅ |ve| ∪. |map_of (rev (zip (map (λv. (v, b)) vs) ds))|"
      unfolding map_upds_def by (intro abs_venv_union)
    also
    have "… ⪅ ve_a  ∪. (⋃. (map (λ(v,k). |[v ↦ k]| ) (zip (map (λv. (v, b)) vs) ds)))"
      using abs_ve abs_venv_map_of_rev
      by (auto intro:smap_union_mono simp add:venv_approx_def)
    also
    have "… = ve_a ∪. (⋃. (map (λ(v,y). |[(v,b) ↦ y]| ) (zip vs ds)))"
      by (auto simp add: zip_map1 o_def split_def)
    also
    have "… ⪅ ve_a ∪. (⋃. (map (λ(v,y). {(v,b_a) := y}.) (zip vs ds_a)))"
    proof-
      from abs_b abs_ds
      have "list_all2 venv_approx (map (λ(v, y). |[(v, b) ↦ y]| ) (zip vs ds))
                                  (map (λ(v, y). {(v,b_a) := y}.) (zip vs ds_a))"
        by (auto simp add: ds_approx_def d_approx_def venv_approx_def abs_venv_singleton list_all2_conv_all_nth intro:smap_singleton_mono list_all2I)
      thus ?thesis
        by (auto simp add:venv_approx_def intro: smap_union_mono[OF smap_less_refl smap_Union_mono])
    qed
    finally
    have "|ve(map (λv. (v, b)) vs [↦] ds)|
          ⪅ ve_a ∪. (⋃. (map (λ(v,y). {(v, b_a) := y}.) (zip vs ds_a)))".
  }
  ultimately
  have prem: "|(c, β(lab ↦ b), ve(map (λv. (v, b)) vs [↦] ds), b)|
        ⪅ (c,  |β|(lab ↦ b_a), ve_a ∪. (⋃.(map (λ(v, y). {(v, b_a) := y}.) (zip vs ds_a))), b_a)"
    using abs_b
    by(auto intro:cstate_approx.intros simp add: abs_cstate.simps)

  show "|evalC⋅(Discr (c, β(lab ↦ b), ve(map (λv. (v, b)) vs [↦] ds), b))|
        ⪅ \<aF>⋅(Discr (PC (Lambda lab vs c, |β| ), ds_a, ve_a, b_a))"
  using Next.hyps(2)[OF prem] ds_a_length
  by (subst a_evalF.simps, simp del:a_evalF.simps a_evalC.simps)

  next
  txt ‹Case Plus›
  fix lab a1 a2 cnt
  assume "isProc cnt"
  assume abs_ds': "[{}, {}, |cnt| ] ⪅ ds_a"
  then obtain a1_a a2_a cnt_a where ds_a: "ds_a = [a1_a, a2_a, cnt_a]" and abs_cnt: "|cnt| ⪅ cnt_a"
    unfolding ds_approx_def
    by (cases ds_a rule:list.exhaust[OF _ list.exhaust[OF _ list.exhaust, of _ _ "λ_ x. x"],  of _ _ "λ_ x. x"])
       (auto simp add:ds_approx_def)

  have new_elem: "|{((lab, [lab ↦ b]), cnt)}| ⪅ {((lab, [lab ↦ b_a]), cont) |cont. cont ∈ cnt_a}"
    using abs_cnt and abs_b
    by (auto simp add:ccache_approx_def d_approx_def)

  have prem: "|(cnt, [DI (a1 + a2)], ve, nb b lab)| ⪅
              (the_elem |cnt|, [{}], ve_a, \<anb> b_a lab)"
    using abs_ve and abs_b
    by (auto intro:fstate_approx.intros simp add:ds_approx_def)

  have "|(evalF⋅(Discr (cnt, [DI (a1 + a2)], ve, nb b lab)))|
       ⪅ \<aF>⋅(Discr (the_elem |cnt|, [{}], ve_a, \<anb> b_a lab))"
    by (rule Next.hyps(1)[OF prem])
  also have "… ⪅ (⋃cnt∈cnt_a. \<aF>⋅(Discr (cnt, [{}], ve_a, \<anb> b_a lab)))"
    using abs_cnt
    by (auto intro: the_elem_is_Proc[OF ‹isProc cnt›] simp del: a_evalF.simps simp add:ccache_approx_def d_approx_def)
  finally
  have old_elems: "|(evalF⋅(Discr (cnt, [DI (a1 + a2)], ve, nb b lab)))|
       ⪅ (⋃cnt∈cnt_a. \<aF>⋅(Discr (cnt, [{}], ve_a, \<anb> b_a lab)))".

  have "|((evalF⋅(Discr (cnt, [DI (a1 + a2)], ve, nb b lab)))
          ∪ {((lab, [lab ↦ b]), cnt)})|
        ⪅ |(evalF⋅(Discr (cnt, [DI (a1 + a2)], ve, nb b lab)))|
          ∪ |{((lab, [lab ↦ b]), cnt)}|"
    by (rule abs_ccache_union)
  also
  have "… ⪅
        (⋃cnt∈cnt_a. \<aF>⋅(Discr (cnt, [{}], ve_a, \<anb> b_a lab)))
        ∪ {((lab, [lab ↦ b_a]), cont) |cont. cont ∈ cnt_a}"
    by (rule Un_mono_approx[OF old_elems new_elem])
  finally
  show "|insert ((lab, [lab ↦ b]), cnt)
                (evalF⋅(Discr (cnt, [DI (a1 + a2)], ve, nb b lab)))|
        ⪅ \<aF>⋅(Discr (PP (prim.Plus lab), ds_a, ve_a, b_a))"
    using ds_a by (subst a_evalF.simps)(auto simp del:a_evalF.simps)
  next

  txt ‹Case If (true branch)›
  fix ct cf v cntt cntf
  assume "isProc cntt"
  assume "isProc cntf"
  assume abs_ds': "[{}, |cntt|, |cntf| ] ⪅ ds_a"
  then obtain v_a cntt_a cntf_a where ds_a: "ds_a = [v_a, cntt_a, cntf_a]"
                              and abs_cntt: "|cntt| ⪅ cntt_a"
                              and abs_cntf: "|cntf| ⪅ cntf_a"
    by (cases ds_a rule:list.exhaust[OF _ list.exhaust[OF _ list.exhaust, of _ _ "λ_ x. x"],  of _ _ "λ_ x. x"])
       (auto simp add:ds_approx_def)

  let ?c = "ct::label" and ?cnt = cntt and ?cnt_a = cntt_a

  have new_elem: "|{((?c, [?c ↦ b]), ?cnt)}| ⪅ {((?c, [?c ↦ b_a]), cont) |cont. cont ∈ ?cnt_a}"
    using abs_cntt and abs_cntf and abs_b 
    by (auto simp add:ccache_approx_def d_approx_def)

  have prem: "|(?cnt, [], ve, nb b ?c)| ⪅
              (the_elem |?cnt|, [], ve_a, \<anb> b_a ?c)"
    using abs_ve and abs_b
    by (auto intro:fstate_approx.intros)

  have "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
       ⪅ \<aF>⋅(Discr (the_elem |?cnt|, [], ve_a, \<anb> b_a ?c))"
    by (rule Next.hyps(1)[OF prem])
  also have "… ⪅ (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))"
    using abs_cntt and abs_cntf
    by (auto intro: the_elem_is_Proc[OF ‹isProc ?cnt›] simp del: a_evalF.simps simp add:ccache_approx_def d_approx_def)

  finally
  have old_elems: "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
       ⪅ (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))".

  have "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))
          ∪ {((?c, [?c ↦ b]), ?cnt)}|
        ⪅ |evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
          ∪ |{((?c, [?c ↦ b]), ?cnt)}|"
    by (rule abs_ccache_union)
  also
  have "… ⪅
        (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))
        ∪ {((?c, [?c ↦ b_a]), cont) |cont. cont ∈ ?cnt_a}"
    by (rule Un_mono_approx[OF old_elems new_elem])
  also
  have "… ⪅
        ((⋃cnt∈cntt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ct)))
          ∪ {((ct, [ct ↦ b_a]), cont) |cont. cont ∈ cntt_a})
      ∪ ((⋃cnt∈cntf_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a cf)))
          ∪ {((cf, [cf ↦ b_a]), cont) |cont. cont ∈ cntf_a})"
    by (rule Un_upper1_approx|rule Un_upper2_approx)
  finally
  show "|insert ((?c, [?c ↦ b]), ?cnt)
                (evalF⋅(Discr (?cnt, [], ve, nb b ?c)))| ⪅
          \<aF>⋅(Discr (PP (prim.If ct cf), ds_a, ve_a, b_a))"
    using ds_a by (subst a_evalF.simps)(auto simp del:a_evalF.simps)
  next

  txt ‹Case If (false branch). We use schematic variable to keep this similar to the true branch.›
  fix ct cf v cntt cntf
  assume "isProc cntt"
  assume "isProc cntf"
  assume abs_ds': "[{}, |cntt|, |cntf| ] ⪅ ds_a"
  then obtain v_a cntt_a cntf_a where ds_a: "ds_a = [v_a, cntt_a, cntf_a]"
                              and abs_cntt: "|cntt| ⪅ cntt_a"
                              and abs_cntf: "|cntf| ⪅ cntf_a"
    by (cases ds_a rule:list.exhaust[OF _ list.exhaust[OF _ list.exhaust, of _ _ "λ_ x. x"],  of _ _ "λ_ x. x"])
       (auto simp add:ds_approx_def)

  let ?c = "cf::label" and ?cnt = cntf and ?cnt_a = cntf_a

  have new_elem: "|{((?c, [?c ↦ b]), ?cnt)}| ⪅ {((?c, [?c ↦ b_a]), cont) |cont. cont ∈ ?cnt_a}"
    using abs_cntt and abs_cntf and abs_b 
    by (auto simp add:ccache_approx_def d_approx_def)

  have prem: "|(?cnt, [], ve, nb b ?c)| ⪅
              (the_elem |?cnt|, [], ve_a, \<anb> b_a ?c)"
    using abs_ve and abs_b
    by (auto intro:fstate_approx.intros)

  have "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
       ⪅ \<aF>⋅(Discr (the_elem |?cnt|, [], ve_a, \<anb> b_a ?c))"
    by (rule Next.hyps(1)[OF prem])
  also have "… ⪅ (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))"
    using abs_cntt and abs_cntf
    by (auto intro: the_elem_is_Proc[OF ‹isProc ?cnt›] simp del: a_evalF.simps simp add:ccache_approx_def d_approx_def)

  finally
  have old_elems: "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
       ⪅ (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))".

  have "|evalF⋅(Discr (?cnt, [], ve, nb b ?c))
          ∪ {((?c, [?c ↦ b]), ?cnt)}|
        ⪅ |evalF⋅(Discr (?cnt, [], ve, nb b ?c))|
          ∪ |{((?c, [?c ↦ b]), ?cnt)}|"
    by (rule abs_ccache_union)
  also
  have "… ⪅
        (⋃cnt∈?cnt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ?c)))
        ∪ {((?c, [?c ↦ b_a]), cont) |cont. cont ∈ ?cnt_a}"
    by (rule Un_mono_approx[OF old_elems new_elem])
  also
  have "… ⪅
        ((⋃cnt∈cntt_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a ct)))
          ∪ {((ct, [ct ↦ b_a]), cont) |cont. cont ∈ cntt_a})
      ∪ ((⋃cnt∈cntf_a. \<aF>⋅(Discr (cnt, [], ve_a, \<anb> b_a cf)))
          ∪ {((cf, [cf ↦ b_a]), cont) |cont. cont ∈ cntf_a})"
    by (rule Un_upper1_approx|rule Un_upper2_approx)
  finally
  show "|insert ((?c, [?c ↦ b]), ?cnt)
                (evalF⋅(Discr (?cnt, [], ve, nb b ?c)))| ⪅
          \<aF>⋅(Discr (PP (prim.If ct cf), ds_a, ve_a, b_a))"
    using ds_a by (subst a_evalF.simps)(auto simp del:a_evalF.simps)
 qed
next
case 2
  obtain c β ve b where cstate: "cstate = (c,β,ve,b)"
    by (cases cstate, auto)
  moreover
  obtain c_a β_a ds_a ve_a b_a where cstate_a: "cstate_a = (c_a,β_a,ve_a,b_a)"
    by (cases cstate_a, auto)
  ultimately
  have abs_c: "c = c_a"
   and abs_β: "|β| = β_a"
   and abs_ve: "|ve| ⪅ ve_a"
   and abs_b: "|b| = b_a"
  using 2 by (auto elim:cstate_approx.cases)

  from cstate cstate_a abs_c abs_β abs_b
  show ?case
  proof(cases c, auto simp add:HOL.Let_def simp del:a_evalF.simps a_evalC.simps set_map evalV.simps)

  txt ‹Case App›
  fix lab f vs
  let ?d = "𝒜 f β ve"
  assume "isProc ?d"

  have "map (abs_d ∘ (λv. 𝒜 v β ve)) vs ⪅ map (λv. \<aA> v β_a ve_a) vs"
    using abs_β and lemma7[OF abs_ve, of _ β]
    by (auto intro!: list_all2I simp add:set_zip ds_approx_def)

  hence "|evalF⋅(Discr (?d, map (λv. 𝒜 v β ve) vs, ve, nb b lab))|
     ⪅ \<aF>⋅(Discr(the_elem |?d|, map (λv. \<aA> v β_a ve_a) vs, ve_a, \<anb> |b| lab))"
    using abs_ve and abs_cnt_nb and abs_b
    by -(rule Next.hyps(1),auto intro:fstate_approx.intros)
  also have "… ⪅ (⋃f'∈\<aA> f β_a ve_a.
              \<aF>⋅(Discr(f', map (λv. \<aA> v β_a ve_a) vs, ve_a, \<anb> |b| lab)))"
    using lemma7[OF abs_ve] the_elem_is_Proc[OF ‹isProc ?d›] abs_β
    by (auto simp del: a_evalF.simps simp add:d_approx_def ccache_approx_def)
  finally
  have old_elems: "
     |evalF⋅(Discr (𝒜 f β ve, map (λv. 𝒜 v β ve) vs, ve, nb b lab))|
     ⪅ (⋃f'∈ \<aA> f β_a ve_a.
              \<aF>⋅(Discr(f', map (λv. \<aA> v β_a ve_a) vs, ve_a, \<anb> |b| lab)))"
    by auto

  have new_elem: "|{((lab, β), 𝒜 f β ve)}|
                  ⪅ {((lab, β_a), f') |f'. f' ∈ \<aA> f β_a ve_a}"
    using abs_β and lemma7[OF abs_ve]
    by(auto simp add:ccache_approx_def d_approx_def)
 
  have "|evalF⋅(Discr (𝒜 f β ve, map (λv. 𝒜 v β ve) vs, ve, nb b lab))
        ∪ {((lab, β), 𝒜 f β ve)}|
        ⪅ |evalF⋅(Discr (𝒜 f β ve, map (λv. 𝒜 v β ve) vs, ve, nb b lab))|
        ∪ |{((lab, β), 𝒜 f β ve)}|"
    by (rule abs_ccache_union)
  also have "…
        ⪅ (⋃f'∈\<aA> f β_a ve_a.
              \<aF>⋅(Discr(f', map (λv. \<aA> v β_a ve_a) vs, ve_a, \<anb> |b| lab)))
        ∪ {((lab, β_a), f') |f'. f' ∈ \<aA> f β_a ve_a}"
    by (rule Un_mono_approx[OF old_elems new_elem])
  finally
  show "|insert ((lab, β), 𝒜 f β ve)
                (evalF⋅(Discr (𝒜 f β ve, map (λv. 𝒜 v β ve) vs, ve, nb b lab)))|
        ⪅ \<aC>⋅(Discr (App lab f vs, |β|, ve_a, |b| ))"
    using abs_β
    by (subst a_evalC.simps)(auto simp add: HOL.Let_def simp del:a_evalF.simps)
  next

  txt ‹Case Let›
  fix lab binds c'

  have "|β(lab ↦ nb b lab)| =
        β_a(lab ↦ \<anb> |b| lab)"
    using abs_β and abs_b
    by simp
  moreover
  have "|map_of (map (λ(v, l). ((v, nb b lab),
                                 DC (l, β(lab ↦ nb b lab))))
                     binds)|
    ⪅ ⋃. (map (λ(v, l).
              {(v, \<anb> |b| lab) :=  {PC (l, β_a(lab ↦ \<anb> |b| lab))}}.)
              binds)"
    using abs_b and abs_β
    apply -
    apply (rule venv_approx_trans[OF abs_venv_map_of])
    apply (auto intro:smap_union_mono list_all2I
              simp add:venv_approx_def o_def set_zip abs_venv_singleton split_def smap_less_refl)
    done
  hence "|ve ++ map_of
            (map (λ(v, l).
                   ((v, nb b lab),
                    DC (l, β(lab ↦ nb b lab))))
                  binds)| ⪅
        ve_a ∪.
        (⋃.
          (map (λ(v, l).
            {(v, \<anb> |b| lab) :=  {PC (l, β_a(lab ↦ \<anb> |b| lab))}}.)
            binds))"
    by (rule venv_approx_trans[OF abs_venv_union
      smap_union_mono[OF abs_ve[unfolded venv_approx_def], folded venv_approx_def]])
  ultimately
  have "|evalC⋅(Discr(c', β(lab ↦ nb b lab),
            ve ++ map_of
                  (map (λ(v, l). ((v, nb b lab), DC (l, β(lab ↦ nb b lab)))) binds),
            nb b lab))|
    ⪅ \<aC>⋅(Discr (c', β_a(lab ↦ \<anb> |b| lab),
            ve_a ∪.
             (⋃. (map (λ(v, l).
                   {(v, \<anb> |b| lab) :=  {PC (l, β_a(lab ↦ \<anb> |b| lab))}}.)
                   binds)),
         \<anb> |b| lab))"
    using abs_cnt_nb and abs_b
    by -(rule Next.hyps(2),auto intro: cstate_approx.intros)

  thus "|evalC⋅(Discr (c', β(lab ↦ nb b lab),
                      ve ++ map_of (map (λ(v, l).((v, nb b lab),𝒜 (L l) (β(lab ↦ nb b lab)) ve)) binds),
                      nb b lab))| ⪅
          \<aC>⋅(Discr (call.Let lab binds c', |β|, ve_a, |b| ))"
    using abs_β
    by (subst a_evalC.simps)(auto simp add: HOL.Let_def simp del:a_evalC.simps)
  qed
}
qed

text ‹
And finally, we lift this result to ‹\<aPR>› and ‹\<PR>›.
›

lemma lemma6: "|\<PR> l| ⪅ \<aPR> l"
  unfolding evalCPS_def evalCPS_a_def
  by (auto intro!:lemma89 fstate_approx.intros simp del:evalF.simps a_evalF.simps
      simp add: ds_approx_def d_approx_def venv_approx_def)
end