Re: [isabelle] Higher-order matching



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.

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.