theory "AList-Utils-HOLCF"
imports "HOLCF-Utils" "HOLCF-Join-Classes" "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 = 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
end