# Re: [isabelle] Higher-order matching

s.wong.731 at googlemail.com schrieb:
> On Sep 1, 2009 8:49am, Tobias Nipkow <nipkow at in.tum.de> wrote:
>> Most of our proof methods will not prove "EX f. ..." automatically when
>>
>> f is a function. In this case "blast" will do it because the situation
>>
>> is trivial. In general, do not expect to prove EX formulas
>>
>> automatically, unless the situation is almost trivial.
>>
>
> I see. In that case, what sort of tactic should be used to prove this
> (if any)? Sorry, I'm very new to Isabelle.
In general you have to write a proper proof. See the Isabelle documentation.
Regards
Tobias
> Thanks
> Steve
>
>>
>>
>> Tobias
>>
>>
>>
>> PS You can drop both "ALL x y" and [rule_format] in ax1.
>>
>>
>>
>> s.wong.731 at googlemail.com schrieb:
>>
>> > Hi,
>>
>> >
>>
>> > I have a rather trivial problem with higher-order matching. Suppose
> I have:
>>
>> >
>>
>> > consts
>>
>> > FuncA :: "X_Int => X_Int"
>>
>> > FuncB :: "X_Int => X_Int"
>>
>> >
>>
>> > axioms
>>
>> > ax1 [rule_format] :
>>
>> > "ALL x y. FuncA(x)
>> >
>>
>> > declare ax1 [simp]
>>
>> >
>>
>> > theorem test1:
>>
>> > "ALL x y. FuncA(x)
>> > using ax1
>>
>> > by (auto)
>>
>> >
>>
>> > The proof succeeds since it's simply applying ax1.
>>
>> >
>>
>> > What about if I want to prove the following:
>>
>> >
>>
>> > theorem test2:
>>
>> > "ALL x y.
>>
>> > EX f.
>>
>> > f(x)
>> > using ax1
>>
>> > by (auto)
>>
>> >
>>
>> > It fails. Am I missing a lemma? If so, what lemma am I missing? Can ax1
>>
>> > not be applied in the same way as in test1?
>>
>> >
>>
>> > Any help will be appreciated.
>>
>> >
>>
>> > Thanks
>>
>> > Steve
>>

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