Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Domain proof

Email Gateway (Aug 19 2022 at 13:33):

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

how can i prove

lemma "dom (SOME b. dom b = A) = A"

Thank you!

Email Gateway (Aug 19 2022 at 13:33):

From: Peter Lammich <lammich@in.tum.de>
On Fr, 2014-01-17 at 18:03 +0200, Roger H. wrote:

Hi,

how can i prove

lemma "dom (SOME b. dom b = A) = A"

You have to show that there is such a beast b, ie,

proof -
obtain b where "dom b = A" ...
thus ?thesis
sledgehammer (*Should find a proof now, using the rules for SOME,
probably SomeI*)

-- Peter

Thank you!

Email Gateway (Aug 19 2022 at 13:33):

From: Manuel Eberl <eberlm@in.tum.de>
On my system, the nicest proof sledgehammer finds (after I provide a
suitable witness, as Peter suggested) is something like "by (metis
(lifting, full_types) dom_const dom_restrict inf_top.left_neutral
someI_ex)", which takes over a second to run.

These proofs often get a bit tricky because Higher Order Unification
does strange things with the someI/someI_ex rules and therefore, one
often has to instantiate them manually. I would prove your lemmas like this:

lemma "dom (SOME b. dom b = A) = A"
by (rule someI_ex[where P = "λb. dom b = A"],
rule exI[where x = "(λ_. Some undefined) |` A"], simp)

Or, alternatively, if you prefer a more readable Isar proof:

lemma "dom (SOME b. dom b = A) = A"
proof-
let ?f = "(λ_. Some undefined) |` A"
have "dom ?f = A" by simp
thus ?thesis by (rule someI[where P = "λb. dom b = A"])
qed

In case you're wondering what "(λ_. Some undefined) | A" is: "(λ_. Some undefined)" is simply a partial function that is defined everywhere and always returns "undefined", which is some fixed value of your codomain type about which you know nothing – except that it exists. | A then
restricts this function to A, i.e. returns "None" everywhere except for
values in A. You could also write "(λx. if x ∈ A then Some undefined
else None)"

Note that without the explicit "where" instantiations in someI and
someI_ex, it does not work because unification does not produce the
unifier I want. In fact, I'm curious as to why this happens myself. Can
anybody explain this?

Cheers,
Manuel

Last updated: Apr 25 2024 at 08:20 UTC