Theory CoCallAnalysisBinds

theory CoCallAnalysisBinds
imports CoCallAnalysisSig AEnv  "AList-Utils-HOLCF" "Arity-Nominal" "CoCallGraph-Nominal"
begin

context CoCallAnalysis
begin
definition ccBind :: "var ⇒ exp ⇒ ((AEnv × CoCalls) → CoCalls)"
  where "ccBind v e = (Λ (ae, G).  if (v--v∉G) ∨ ¬ isVal e then cc_restr (fv e) (fup⋅(ccExp e)⋅(ae v)) else ccSquare (fv e))"
(* paper has:  ∨ ae v = up⋅0, but that is not monotone! But should give the same result. *)

lemma ccBind_eq:
  "ccBind v e⋅(ae, G) = (if v--v∉G ∨ ¬ isVal e then 𝒢⇧^⊥⇘ae v⇙ e G|` fv e else (fv e)⇧²)"
  unfolding ccBind_def
  apply (rule cfun_beta_Pair)
  apply (rule cont_if_else_above)
  apply simp
  apply simp
  apply (auto dest: subsetD[OF ccField_cc_restr])[1]
  (* Abstraction broken! Fix this. *)
  apply (case_tac p, auto, transfer, auto)[1]
  apply (rule adm_subst[OF cont_snd])
  apply (rule admI, thin_tac "chain _", transfer, auto)
  done

lemma ccBind_strict[simp]: "ccBind v e ⋅ ⊥ = ⊥"
  by (auto simp add: inst_prod_pcpo ccBind_eq simp del: Pair_strict)

lemma ccField_ccBind: "ccField (ccBind v e⋅(ae,G)) ⊆ fv e"
  by (auto simp add: ccBind_eq dest: subsetD[OF ccField_cc_restr])

definition ccBinds :: "heap ⇒ ((AEnv × CoCalls) → CoCalls)"
  where "ccBinds Γ = (Λ i. (⨆v↦e∈map_of Γ. ccBind v e⋅i))"

lemma ccBinds_eq:
  "ccBinds Γ⋅i = (⨆v↦e∈map_of Γ. ccBind v e⋅i)"
  unfolding ccBinds_def
  by simp

lemma ccBinds_strict[simp]: "ccBinds Γ⋅⊥=⊥"
  unfolding ccBinds_eq
  by (cases "Γ = []") simp_all

lemma ccBinds_strict'[simp]: "ccBinds Γ⋅(⊥,⊥)=⊥"
  by (metis CoCallAnalysis.ccBinds_strict Pair_bottom_iff)

lemma ccBinds_reorder1:
  assumes "map_of Γ v = Some e"
  shows "ccBinds Γ = ccBind v e ⊔ ccBinds (delete v Γ)"
proof-
  from assms 
  have "map_of Γ = map_of ((v,e) # delete v Γ)" by (metis map_of_delete_insert)
  thus ?thesis
    by (auto intro: cfun_eqI simp add: ccBinds_eq delete_set_none)
qed

lemma ccBinds_Nil[simp]:
  "ccBinds [] = ⊥"
  unfolding ccBinds_def by simp

lemma ccBinds_Cons[simp]:
   "ccBinds ((x,e)#Γ) = ccBind x e ⊔ ccBinds (delete x Γ)"
   by (subst ccBinds_reorder1[where v = x and e = e]) auto

lemma ccBind_below_ccBinds: "map_of Γ x = Some e ⟹ ccBind x e⋅ae ⊑ (ccBinds Γ⋅ae)"
  by (auto simp add: ccBinds_eq)

lemma ccField_ccBinds: "ccField (ccBinds Γ⋅(ae,G)) ⊆ fv Γ"
  by (auto simp add: ccBinds_eq dest: subsetD[OF ccField_ccBind] intro: subsetD[OF map_of_Some_fv_subset])

definition ccBindsExtra :: "heap ⇒ ((AEnv × CoCalls) → CoCalls)"
  where "ccBindsExtra Γ = (Λ i.  snd i ⊔ ccBinds Γ ⋅ i  ⊔ (⨆x↦e∈map_of Γ. ccProd (fv e) (ccNeighbors x (snd i))))"

lemma ccBindsExtra_simp: "ccBindsExtra Γ ⋅ i =snd i ⊔ ccBinds Γ ⋅ i ⊔ (⨆x↦e∈map_of Γ. ccProd (fv e) (ccNeighbors x (snd i)))"
  unfolding ccBindsExtra_def by simp

lemma ccBindsExtra_eq: "ccBindsExtra Γ⋅(ae,G) =
  G ⊔ ccBinds Γ⋅(ae,G) ⊔ (⨆x↦e∈map_of Γ. fv e G× ccNeighbors x G)"
  unfolding ccBindsExtra_def by simp

lemma ccBindsExtra_strict[simp]: "ccBindsExtra Γ ⋅ ⊥ = ⊥"
  by (auto simp add: ccBindsExtra_simp inst_prod_pcpo simp del: Pair_strict)

lemma ccField_ccBindsExtra:
  "ccField (ccBindsExtra Γ⋅(ae,G)) ⊆ fv Γ ∪ ccField G"
  by (auto simp add: ccBindsExtra_simp elem_to_ccField
      dest!:  subsetD[OF ccField_ccBinds]  subsetD[OF ccField_ccProd_subset] map_of_Some_fv_subset)

end

lemma ccBind_eqvt[eqvt]: "π ∙ (CoCallAnalysis.ccBind cccExp x e) = CoCallAnalysis.ccBind (π ∙ cccExp) (π ∙ x) (π ∙ e)"
proof-
  {
  fix π ae G
  have "π ∙ ((CoCallAnalysis.ccBind cccExp x e) ⋅ (ae,G)) = CoCallAnalysis.ccBind (π ∙ cccExp) (π ∙ x) (π ∙ e) ⋅ (π ∙ ae, π ∙ G)"
    unfolding CoCallAnalysis.ccBind_eq
    by perm_simp (simp add: Abs_cfun_eqvt)
  }
  thus ?thesis by (auto intro: cfun_eqvtI)
qed

lemma ccBinds_eqvt[eqvt]: "π ∙ (CoCallAnalysis.ccBinds cccExp Γ) = CoCallAnalysis.ccBinds (π ∙ cccExp) (π ∙ Γ)"
  apply (rule cfun_eqvtI)
  unfolding CoCallAnalysis.ccBinds_eq
  apply (perm_simp) 
  apply rule
  done

lemma ccBindsExtra_eqvt[eqvt]: "π ∙ (CoCallAnalysis.ccBindsExtra cccExp Γ) = CoCallAnalysis.ccBindsExtra (π ∙ cccExp) (π ∙ Γ)"
  by (rule cfun_eqvtI) (simp add: CoCallAnalysis.ccBindsExtra_def)

lemma ccBind_cong[fundef_cong]:
  "cccexp1 e = cccexp2 e ⟹ CoCallAnalysis.ccBind cccexp1 x e = CoCallAnalysis.ccBind cccexp2 x e "
  apply (rule cfun_eqI)
  apply (case_tac xa)
  apply (auto simp add: CoCallAnalysis.ccBind_eq)
  done

lemma ccBinds_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧
      ⟹ CoCallAnalysis.ccBinds cccexp1 heap1 = CoCallAnalysis.ccBinds cccexp2 heap2"
  apply (rule cfun_eqI)
  unfolding CoCallAnalysis.ccBinds_eq
  apply (rule arg_cong[OF mapCollect_cong])
  apply (rule arg_cong[OF ccBind_cong])
  apply auto
  by (metis imageI map_of_SomeD snd_conv)

lemma ccBindsExtra_cong[fundef_cong]:
  "⟦ (⋀ e. e ∈ snd ` set heap2 ⟹ cccexp1 e = cccexp2 e); heap1 = heap2 ⟧
      ⟹ CoCallAnalysis.ccBindsExtra cccexp1 heap1 = CoCallAnalysis.ccBindsExtra cccexp2 heap2"
  apply (rule cfun_eqI)
  unfolding CoCallAnalysis.ccBindsExtra_simp
  apply (rule arg_cong2[OF ccBinds_cong mapCollect_cong]) 
  apply simp+
  done

end