Email Gateway (Aug 18 2022 at 11:59): Email Gateway (Aug 18 2022 at 11:59):From: John Matthews <matthews@galois.com>
I've come across some strange behavior with the arith proof method in
Isabelle2007. It is able to prove the following lemma:
lemma "[| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"
(Here f is a free variable). However, if I turn x into a parameter of
the subgoal, then arith fails:
lemma "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"
On the other hand, if I replace (f x) with z, then it works again:
lemma "!!x. [| 0 <= (x::int); x div 2 < z |] ==> x < z * 2"
Thanks,
-john
Email Gateway (Aug 18 2022 at 12:01):From: Tobias Nipkow <nipkow@in.tum.de>
Thank you, that should not be the case, will look into it (at some point).
Tobias
John Matthews schrieb:
Last updated: May 03 2024 at 08:18 UTC