finite_map_elems_card.thy

lemma finite_map_elems_card:
  assumes "finite {(a, b). m a = Some b}"
  shows "card {(a, b). m a = Some b} = card (Map.dom m)" (is "card ?E = card ?D")
proof-
  have "Map.dom m = fst ` ?E"
    apply (simp add: Map.dom_def)
    by force
  hence de: "card ?D ≤ card ?E"
    by (simp add: assms card_image_le)

  have e_alt: "{(a, b). m a = Some b} = (λ a. (a, the (m a))) ` Map.dom m"
    by fastforce

  have "∀ (a, b) ∈ ?E. ¬ (∃ c. b ≠ c ∧ (a, c) ∈ ?E)"
    by auto
  hence ed: "card ?E ≤ card ?D"
    by (metis `?D = fst \` ?E` assms card_image_le e_alt finite_imageI)

  show ?thesis
    using antisym_conv ed de
    by blast
qed