[isabelle] Unifying existentially quantified function



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.