[isabelle] Unifying existentially quantified function
For the following:
f :: "real => real" and
c :: real
ax : "f c = 0"
theorem "EX (func::real => real) x. func x = 0"
apply (intro exI)
apply (rule ax)
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)) %%
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and