Theory ExCFSV

section ‹The exact call cache is a map›

theory ExCFSV
imports ExCF
begin

subsection ‹Preparations›

text ‹
Before we state the main result of this section, we need to define
\begin{itemize}
\item the set of binding environments occurring in a semantic value (which exists only if it is a closure),
\item the set of binding environments in a variable environment, using the previous definition,
\item the set of contour counters occurring in a semantic value and
\item the set of contour counters occurring in a variable environment.
\end{itemize}
›

fun benv_in_d :: "d ⇒ benv set"
  where "benv_in_d (DC (l,β)) = {β}"
      | "benv_in_d _ = {}"

definition benv_in_ve :: "venv ⇒ benv set"
  where "benv_in_ve ve = ⋃{benv_in_d d | d . d ∈ ran ve}"

fun contours_in_d :: "d ⇒ contour set"
  where "contours_in_d (DC (l,β)) = ran β"
      | "contours_in_d _ = {}"

definition contours_in_ve :: "venv ⇒ contour set"
  where "contours_in_ve ve = ⋃{contours_in_d d | d . d ∈ ran ve}"

text ‹
The following 6 lemmas allow us to calculate the above definition, when applied to constructs used in our semantics function, e.g. map updates, empty maps etc.
›

lemma benv_in_ve_upds:
  assumes eq_length: "length vs = length ds"
      and "∀β∈benv_in_ve ve. Q β"
      and "∀d'∈set ds. ∀β∈benv_in_d d'. Q β"
  shows   "∀β∈benv_in_ve (ve(map (λv. (v, b'')) vs [↦] ds)). Q β"
proof
  fix β
  assume ass:"β ∈ benv_in_ve (ve(map (λv. (v, b'')) vs [↦] ds))"
  then obtain d where "β∈benv_in_d d" and "d ∈ ran (ve(map (λv. (v, b'')) vs [↦] ds))" unfolding benv_in_ve_def by auto
  moreover have "ran (ve(map (λv. (v, b'')) vs [↦] ds)) ⊆ ran ve ∪ set ds" using eq_length by(auto intro!:ran_upds) 
  ultimately
  have "d ∈ ran ve ∨ d ∈ set ds" by auto
  thus "Q β" using assms(2,3) ‹β∈benv_in_d d› unfolding benv_in_ve_def by auto
qed

lemma benv_in_eval:
  assumes "∀β'∈benv_in_ve ve. Q β'"
      and "Q β"
  shows "∀β∈benv_in_d (𝒜 v β ve). Q β"
proof(cases v)
  case (R _ var)
  thus ?thesis
  proof (cases "β (fst var)")
    case None with R show ?thesis by simp next
    case (Some cnt) show ?thesis
    proof (cases "ve (var,cnt)")
      case None with Some R show ?thesis by simp next
      case (Some d)
        hence "d ∈ ran ve" unfolding ran_def by blast
        thus ?thesis using Some ‹β (fst var) = Some cnt› R assms(1)
          unfolding benv_in_ve_def by auto
    qed
  qed next
  case (L l) thus ?thesis using assms(2) by simp next
  case C thus ?thesis by simp next
  case P thus ?thesis by simp
qed

lemma contours_in_ve_empty[simp]: "contours_in_ve Map.empty = {}"
  unfolding contours_in_ve_def by auto

lemma contours_in_ve_upds:
  assumes eq_length: "length vs = length ds"
      and "∀b'∈contours_in_ve ve. Q b'"
      and "∀d'∈set ds. ∀b'∈contours_in_d d'. Q b'"
  shows   "∀b'∈contours_in_ve (ve(map (λv. (v, b'')) vs [↦] ds)). Q b'"
proof-
  have "ran (ve(map (λv. (v, b'')) vs [↦] ds)) ⊆ ran ve ∪ set ds" using eq_length by(auto intro!:ran_upds)
  thus ?thesis using assms(2,3) unfolding contours_in_ve_def  by blast
qed

lemma contours_in_ve_upds_binds:
  assumes "∀b'∈contours_in_ve ve. Q b'"
      and "∀b'∈ran β'. Q b'"
  shows   "∀b'∈contours_in_ve (ve ++ map_of (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls)). Q b'"
proof
  fix b' assume "b'∈contours_in_ve (ve ++ map_of (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls))"
  then obtain d where d:"d ∈ ran (ve ++ map_of (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls))" and b:"b' ∈ contours_in_d d" unfolding contours_in_ve_def by auto
  
  have "ran (ve ++ map_of (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls)) ⊆ ran ve ∪ ran (map_of (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls))"
    by(auto intro!:ran_concat)
  also
  have "… ⊆ ran ve ∪ snd ` set (map (λ(v,l). ((v,b''), 𝒜 (L l) β' ve)) ls)"
    by (rule Un_mono[of "ran ve" "ran ve", OF subset_refl ran_map_of])
  also
  have "… ⊆ ran ve ∪ set (map (λ(v,l). (𝒜 (L l) β' ve)) ls)"
    by (rule Un_mono[of "ran ve" "ran ve", OF subset_refl ])auto
  finally
  have "d ∈  ran ve ∪ set (map (λ(v,l). (𝒜 (L l) β' ve)) ls)" using d by auto
  thus "Q b'"  using assms b unfolding contours_in_ve_def by auto
qed

lemma contours_in_eval:
  assumes "∀b'∈contours_in_ve ve. Q b'"
      and "∀b'∈ ran β. Q b'"
  shows "∀b'∈contours_in_d (𝒜 f β ve). Q b'"
unfolding contours_in_ve_def
proof(cases f)
  case (R _ var)
  thus ?thesis
  proof (cases "β (fst var)")
    case None with R show ?thesis by simp next
    case (Some cnt) show ?thesis
    proof (cases "ve (var,cnt)")
      case None with Some R show ?thesis by simp next
      case (Some d)
        hence "d ∈ ran ve" unfolding ran_def by blast
        thus ?thesis using Some ‹β (fst var) = Some cnt› R ‹∀b'∈contours_in_ve ve. Q b'›
          unfolding contours_in_ve_def
          by auto
    qed
  qed next
  case (L l) thus ?thesis using ‹∀b'∈ ran β. Q b'› by simp next
  case C thus ?thesis by simp next
  case P thus ?thesis by simp
qed

subsection ‹The proof›

text ‹
The set returned by ‹ℱ› and ‹𝒞› is actually a partial map from callsite/binding environment pairs to called values. The corresponding predicate in Isabelle is ‹single_valued›.

We would like to show an auxiliary result about the contour counter passed to ‹ℱ› and ‹𝒞› (such that it is an unused counter when passed to ‹ℱ› and others) first. Unfortunately, this is not possible with induction proofs over fixed points: While proving the inductive case, one does not show results for the function in question, but for an information-theoretical approximation. Thus, any previously shown results are not available.
We therefore intertwine the two inductions in one large proof.

This is a proof by fixpoint induction, so we have are obliged to show that the predicate is admissible and that it holds for the base case, i.e. the empty set. For the proof of admissibiliy, @{theory HOLCF} provides a number of introduction lemmas that, together with some additions in @{theory "Shivers-CFA.HOLCFUtils"} and the continuity lemmas, mechanically proove admissibiliy. The base case is trivial.

The remaining case is the preservation of the properties when applying the recursive equations to a function known to have have the desired property. Here, we break the proof into the various cases that occur in the definitions of ‹ℱ› and ‹𝒞› and use the induction hypothesises.
›

lemma cc_single_valued':
      "⟦ ∀b' ∈ contours_in_ve ve. b' < b
       ; ∀b' ∈ contours_in_d d. b' < b
       ; ∀d' ∈ set ds. ∀b' ∈ contours_in_d d'. b' < b
       ⟧
       ⟹
       (   single_valued (ℱ⋅(Discr (d,ds,ve,b)))
       ∧ (∀ ((lab,β),t) ∈ ℱ⋅(Discr (d,ds,ve, b)). ∃ b'. b' ∈ ran β ∧ b ≤ b')
       )"
  and "⟦ b ∈ ran β'
       ; ∀b'∈ran β'. b' ≤ b
       ; ∀b' ∈ contours_in_ve ve. b' ≤ b
       ⟧
       ⟹
       (   single_valued (𝒞⋅(Discr (c,β',ve,b)))
       ∧ (∀ ((lab,β),t) ∈ 𝒞⋅(Discr (c,β',ve,b)). ∃ b'. b' ∈ ran β ∧ b ≤ b')
       )"
proof(induct arbitrary:d ds ve b c β' rule:evalF_evalC_induct)
case Admissibility show ?case
  by (intro adm_lemmas adm_ball' adm_prod_split adm_not_conj adm_not_mem adm_single_valued cont2cont)
next
  case Bottom {
    case 1 thus ?case by auto next
    case 2 thus ?case by auto
  }
next
  case (Next evalF evalC)

  txt ‹Nicer names for the hypothesises:›
  note hyps_F_sv = Next.hyps(1)[THEN conjunct1]
  note hyps_F_b = Next.hyps(1)[THEN conjunct2, THEN bspec]
  note hyps_C_sv = Next.hyps(2)[THEN conjunct1]
  note hyps_C_b = Next.hyps(2)[THEN conjunct2, THEN bspec]
  {
  case (1 d ds ve b)
  thus ?case
  proof (cases "(d,ds,ve,b)" rule:fstate_case, auto simp del:Un_insert_left Un_insert_right)
  txt ‹Case Closure›
    fix lab' and vs :: "var list" and c and β' :: benv
    assume prem_d: "∀b'∈ran β'. b' < b"
    assume eq_length: "length vs = length ds"
    have new: "b∈ran (β'(lab' ↦ b))" by simp

    have b_dom_beta: "∀b'∈ ran (β'(lab' ↦ b)). b' ≤ b"
    proof fix b' assume "b' ∈ ran (β'(lab' ↦ b))"
      hence "b' ∈ ran β' ∨ b' ≤ b" by (auto dest:ran_upd[THEN subsetD])
      thus "b' ≤ b" using prem_d by auto
    qed
    from contours_in_ve_upds[OF eq_length "1.prems"(1) "1.prems"(3)]
    have b_dom_ve: "∀b'∈contours_in_ve (ve(map (λv. (v, b)) vs [↦] ds)). b' ≤ b"
      by auto

    show "single_valued (evalC⋅(Discr (c, β'(lab' ↦ b), ve(map (λv. (v, b)) vs [↦] ds), b)))"
      by (rule hyps_C_sv[OF new b_dom_beta b_dom_ve, of c])

    fix lab and β and t
    assume "((lab, β), t)∈ evalC⋅(Discr(c, β'(lab' ↦ b), ve(map (λv. (v, b)) vs [↦] ds),b))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by (auto dest: hyps_C_b[OF new b_dom_beta b_dom_ve])
  next
  txt ‹Case Plus›
    fix cp and i1 and i2 and cnt
    assume "∀b'∈contours_in_d cnt. b' < b"
    hence b_dom_d: "∀b'∈contours_in_d cnt. b' < nb b cp" by auto
    have b_dom_ds: "∀d' ∈ set [DI (i1+i2)]. ∀b'∈contours_in_d d'. b' < nb b cp" by auto
    have b_dom_ve: "∀b' ∈ contours_in_ve ve. b' < nb b cp" using "1.prems"(1) by auto
    {
      fix t
      assume "((cp,[cp ↦ b]), t) ∈ evalF⋅(Discr (cnt, [DI (i1 + i2)], ve, nb b cp))"
      hence False by (auto dest:hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
    }
    with hyps_F_sv[OF b_dom_ve b_dom_d b_dom_ds]
    show "single_valued ((evalF⋅(Discr (cnt, [DI (i1 + i2)], ve, nb b cp)))
                      ∪ {((cp, [cp ↦ b]), cnt)})"
      by (auto intro:single_valued_insert)

    fix lab β t
    assume "((lab, β), t) ∈ evalF⋅(Discr (cnt, [DI (i1 + i2)], ve, nb b cp))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by (auto dest: hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
  next
  txt ‹Case If (true branch)›
    fix cp1 cp2 i cntt cntf
    assume "∀b'∈contours_in_d cntt. b' < b"
    hence b_dom_d: "∀b'∈contours_in_d cntt. b' < nb b cp1" by auto
    have b_dom_ds: "∀d' ∈ set []. ∀b'∈contours_in_d d'. b' < nb b cp1" by auto
    have b_dom_ve: "∀b' ∈ contours_in_ve ve. b' < nb b cp1" using "1.prems"(1) by auto
    {
      fix t
      assume "((cp1,[cp1 ↦ b]), t) ∈ evalF⋅(Discr (cntt, [], ve, nb b cp1))"
      hence False by (auto dest:hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
    }
    with Next.hyps(1)[OF b_dom_ve b_dom_d b_dom_ds, THEN conjunct1]
    show "single_valued ((evalF⋅(Discr (cntt, [], ve, nb b cp1)))
                       ∪ {((cp1, [cp1 ↦ b]), cntt)})"
      by (auto intro:single_valued_insert)

    fix lab β t
    assume "((lab, β), t) ∈ evalF⋅(Discr (cntt, [], ve, nb b cp1))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by (auto dest: hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
  next
  txt ‹Case If (false branch). Variable names swapped for easier code reuse.›
    fix cp2 cp1 i cntf cntt
    assume "∀b'∈contours_in_d cntt. b' < b"
    hence b_dom_d: "∀b'∈contours_in_d cntt. b' < nb b cp1" by auto
    have b_dom_ds: "∀d' ∈ set []. ∀b'∈contours_in_d d'. b' < nb b cp1" by auto
    have b_dom_ve: "∀b' ∈ contours_in_ve ve. b' < nb b cp1" using "1.prems"(1) by auto
    {
      fix t
      assume "((cp1,[cp1 ↦ b]), t) ∈ evalF⋅(Discr (cntt, [], ve, nb b cp1))"
      hence False by (auto dest:hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
    }
    with Next.hyps(1)[OF b_dom_ve b_dom_d b_dom_ds, THEN conjunct1]
    show "single_valued ((evalF⋅(Discr (cntt, [], ve, nb b cp1)))
                       ∪ {((cp1, [cp1 ↦ b]), cntt)})"
      by (auto intro:single_valued_insert)

    fix lab β t
    assume "((lab, β), t) ∈ evalF⋅(Discr (cntt, [], ve, nb b cp1))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by (auto dest: hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
  qed
next
  case (2 ve b c β')
  thus ?case
  proof (cases c, auto simp add:HOL.Let_def simp del:Un_insert_left Un_insert_right evalV.simps)
  txt ‹Case App›
    fix lab' f vs

    have prem2': "∀b'∈ran β'. b' < nb b lab'" using "2.prems"(2) by auto
    have prem3': "∀b'∈contours_in_ve ve. b' < nb b lab'" using "2.prems"(3) by auto
    note c_in_e = contours_in_eval[OF prem3' prem2']

    have b_dom_d: "∀b'∈contours_in_d (evalV f β' ve). b' < nb b lab'" by(rule c_in_e)
    have b_dom_ds: "∀d' ∈ set (map (λv. evalV v β' ve) vs). ∀b'∈contours_in_d d'. b' < nb b lab'"
      using c_in_e by auto
    have b_dom_ve: "∀b' ∈ contours_in_ve ve. b' < nb b lab'" by (rule prem3')

    have "∀y. ((lab', β'), y) ∉ evalF⋅(Discr (evalV f β' ve, map (λv. evalV v β' ve) vs, ve, nb b lab'))"
    proof(rule allI, rule notI)
      fix y assume "((lab', β'), y) ∈ evalF⋅(Discr (evalV f β' ve, map (λv. evalV v β' ve) vs, ve, nb b lab'))"
      hence "∃b'. b' ∈ ran β' ∧ nb b lab' ≤ b'"
        by (auto dest: hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
      thus False using prem2' by (auto iff:less_le_not_le)
    qed

    with hyps_F_sv[OF b_dom_ve b_dom_d b_dom_ds]
    show "single_valued (evalF⋅(Discr (evalV f β' ve, map (λv. evalV v β' ve) vs, ve, nb b lab'))
                       ∪ {((lab', β'), evalV f β' ve)})"
      by(auto intro:single_valued_insert)

    fix lab β t
    assume "((lab, β), t) ∈ (evalF⋅(Discr (evalV f β' ve, map (λv. evalV v β' ve) vs, ve, nb b lab')))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by (auto dest: hyps_F_b[OF b_dom_ve b_dom_d b_dom_ds])
  next
  txt ‹Case Let›
    fix lab' ls c'
    have prem2': "∀b'∈ran (β'(lab' ↦ nb b lab')). b' ≤ nb b lab'"
    proof
      fix b' assume "b'∈ran (β'(lab' ↦ nb b lab'))"
      hence "b' ∈ ran β' ∨ b' = nb b lab'" by (auto dest:ran_upd[THEN subsetD])
      thus "b' ≤ nb b lab'" using "2.prems"(2) by auto
    qed
    have prem3': "∀b'∈contours_in_ve ve. b' ≤ nb b lab'" using "2.prems"(3)
      by auto

    note c_in_e = contours_in_eval[OF prem3' prem2']
    note c_in_ve' = contours_in_ve_upds_binds[OF prem3' prem2']

    have b_dom_ve: "∀b' ∈ contours_in_ve (ve ++ map_of (map (λ(v,l). ((v,nb b lab'), evalV (L l) ((β'(lab' ↦ nb b lab'))) ve)) ls)). b' ≤ nb b lab'"
      by (rule c_in_ve')
    have b_dom_beta: "∀b'∈ran (β'(lab' ↦ nb b lab')). b' ≤ nb b lab'" by (rule prem2')
    have new: "nb b lab' ∈ ran (β'(lab' ↦ nb b lab'))" by simp
      
    from hyps_C_sv[OF new b_dom_beta b_dom_ve, of c']
    show "single_valued (evalC⋅(Discr (c', β'(lab' ↦ nb b lab'),
       ve ++ map_of (map (λ(v, l).((v, nb b lab'), evalV (L l) (β'(lab' ↦ nb b lab')) ve))ls),
       nb b lab')))".
    
    fix lab β t 
    assume "((lab, β), t) ∈ evalC⋅(Discr (c', β'(lab' ↦ nb b lab'),
       ve ++ map_of (map (λ(v, l).((v, nb b lab'), 𝒜 (L l) (β'(lab' ↦ nb b lab')) ve))ls),
       nb b lab'))"
    thus "∃b'. b' ∈ ran β ∧ b ≤ b'"
      by -(drule hyps_C_b[OF new b_dom_beta b_dom_ve], auto)
  qed
 }
qed

lemma "single_valued (\<PR> prog)"
unfolding evalCPS_def
by ((subst HOL.Let_def)+, rule cc_single_valued'[THEN conjunct1], auto)
end