Theory AList-Utils-HOLCF

theory "AList-Utils-HOLCF"
imports "Launchbury.HOLCF-Utils" "Launchbury.HOLCF-Join-Classes" "Launchbury.AList-Utils"
begin

syntax
  "_BLubMap" :: "[pttrn, pttrn, 'a ⇀ 'b, 'b] ⇒ 'b" ("(3⨆/_/↦/_/∈/_/./ _)" [0,0,0, 10] 10)

translations
  "⨆ k↦v∈m. e" == "CONST lub (CONST mapCollect (λk v . e) m)"

lemma below_lubmapI[intro]:
  "m k = Some v ⟹ (e k v::'a::Join_cpo) ⊑ (⨆ k↦v∈m. e k v)"
unfolding mapCollect_def by auto

lemma lubmap_belowI[intro]:
  "(⋀ k v . m k = Some v ⟹ (e k v::'a::Join_cpo) ⊑ u) ⟹ (⨆ k↦v∈m. e k v) ⊑ u"
unfolding mapCollect_def by auto

lemma lubmap_const_bottom[simp]:
  "(⨆ k↦v∈m. ⊥) = (⊥::'a::Join_cpo)"
  by (cases "m = Map.empty") auto

lemma lubmap_map_upd[simp]:
  fixes e :: "'a ⇒ 'b ⇒ ('c :: Join_cpo)"
  shows "(⨆k↦v∈m(k' ↦ v'). e k v) = e k' v' ⊔ (⨆k↦v∈m(k':=None). e k v)"
  by simp

lemma lubmap_below_cong:
  assumes "⋀ k v. m k = Some v ⟹ f1 k v ⊑ (f2 k v :: 'a :: Join_cpo)"
  shows "(⨆ k↦v∈m. f1 k v) ⊑ (⨆ k↦v∈m. f2 k v)"
  apply (rule lubmap_belowI)
  apply (rule below_trans[OF assms], assumption)
  apply (rule below_lubmapI, assumption)
  done

lemma cont2cont_lubmap[simp, cont2cont]:
  assumes "(⋀k v . cont (f k v))"
  shows "cont (λx. ⨆ k↦v∈m. (f k v x) :: 'a :: Join_cpo)"
proof (rule contI2)
  show "monofun (λx. ⨆k↦v∈m. f k v x)"
    apply (rule monofunI)
    apply (rule lubmap_below_cong)
    apply (erule cont2monofunE[OF assms])
    done
next
  fix Y :: "nat ⇒ 'd"
  assume "chain Y"
  assume "chain (λi. ⨆k↦v∈m. f k v (Y i))"

  show "(⨆k↦v∈m. f k v (⨆ i. Y i)) ⊑ (⨆ i. ⨆k↦v∈m. f k v (Y i))"
    apply (subst cont2contlubE[OF assms ‹chain Y›])
    apply (rule lubmap_belowI)
    apply (rule lub_mono[OF ch2ch_cont[OF assms ‹chain Y›] ‹chain (λi. ⨆k↦v∈m. f k v (Y i))›])
    apply (erule below_lubmapI)
    done
qed

(*
syntax
  "_BLubMapFilter" :: "[pttrn, pttrn, 'a ⇀ 'b, 'b, bool] ⇒ 'b" ("(3⨆/_/↦/_/∈/_/./ _/ |/ _)" [0,0,0,10,10] 10)

translations
  "⨆ k↦v∈m. e | P" == "CONST lub (CONST mapCollectFilter (λk v. (P,e)) m)"
*)


end