Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Quantifier over empty set

view this post on Zulip Email Gateway (Aug 19 2022 at 13:26):

From: "Roger H." <s57076@hotmail.com>
Hi,

how can i write and prove:

"A = ∅ ⟹ (∀c∈dom A. B) = B "

Thanks

view this post on Zulip Email Gateway (Aug 19 2022 at 13:26):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Roger,

If the symbol ∅ denotes the empty map Map.empty, then you cannot. dom ∅ = {}, so you
quantify over an empty set, and this is always True, even if B is False.

Andreas

Last updated: Apr 26 2024 at 04:17 UTC