Email Gateway (Aug 18 2022 at 13:58): Email Gateway (Aug 18 2022 at 13:58):From: s.wong.731@googlemail.com
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
Email Gateway (Aug 18 2022 at 13:59):From: Tobias Nipkow <nipkow@in.tum.de>
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@googlemail.com schrieb:
Email Gateway (Aug 18 2022 at 14:00):From: Tobias Nipkow <nipkow@in.tum.de>
s.wong.731@googlemail.com schrieb:
On Sep 1, 2009 8:49am, Tobias Nipkow <nipkow@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
SteveTobias
PS You can drop both "ALL x y" and [rule_format] in ax1.
s.wong.731@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 ax1by (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 ax1by (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
Email Gateway (Aug 18 2022 at 14:02):From: s.wong.731@googlemail.com
On Sep 1, 2009 8:49am, Tobias Nipkow <nipkow@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@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
Last updated: Apr 26 2024 at 20:16 UTC