Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unifying existentially quantified function

view this post on Zulip Email Gateway (Aug 18 2022 at 16:02):

From: John Munroe <munddr@gmail.com>
Hi all,

For the following:

axiomatization
f :: "real => real" and
c :: real
where
ax : "f c = 0"

theorem "EX (func::real => real) x. func x = 0"
apply (intro exI)
apply (rule ax)
prf;
done

The partial proof gives:

protectI % EX func x. func x = 0 %%
(exI % (%x. EX xa. x xa = 0) % (%a. a) %% (OfClass type_class %
TYPE(real => real)) %%
(exI % (%x. x = 0) % f c %% (OfClass type_class % TYPE(real)) %%
thm.Test.ax))

Thus, func is unified to %a. a in the proof. Are there ways to make
func unify to f instead? If I'll need my own tactic, then is there a
current implementation that I can use as a reference?

Thanks for the help.
John

Last updated: Apr 24 2024 at 04:17 UTC