Re: [isabelle] Higher-order matching



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.

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) <' FuncB(y)"
> 
> declare ax1 [simp]
> 
> theorem test1:
> "ALL x y. FuncA(x) <' FuncB(y)"
> 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) <' FuncB(y)"
> 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.