# 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.