Re: [isabelle] Infinity - infinity = infinity
Another idea of mine was to embed the extended numbers into the non-standard numbers. The
idea was to do this embedding in a simproc and run linarith on the embedded terms. The
embedding only works if some case analyses are done (in particular for terms like \infty -
\infty), but I guess that one can save some case analyses this way. But the details have
not been worked out so far.
On 02/12/16 17:14, Johannes HÃlzl wrote:
Another idea from Tobias (and I think also Andreas) is to add a special
simpproc which does case-distinction on enat/ereal/ennreal and calls
linarith. I would assume the simpproc is quite slow but can be disable
by default and just be activated by the user.
Am Freitag, den 02.12.2016, 16:57 +0100 schrieb Tobias Nipkow:
Jasmin, there is a reason why I would not do this:
Aless Lasaruk and Thomas Sturm.
Effective Quantifier Elimination for Presburger Arithmetic with
This paper shows that our current enat has quantifier elimination
have not inplemented it, and it would be some work, but not
their system, "â - â = â". Unless we know that your proposed
has quantifier elimination, I would be reluctant to give up that
On 02/12/2016 16:01, Jasmin Blanchette wrote:
As noted before on this mailing list, automation for "enat"
("Library/Extended_Nat.thy") is quite poor. Often, the only way to
proceed is to perform case distinctions on all "enat" and use auto
on the emerging subgoals.
My impression is that many type classes are not available because
of the definition of subtraction. Because "â - â = â" (where "â" is
the infinity symbol), we lack one of the two properties required by
1. âa b. a + b - a = b
2. âa b c. a - b - c = a - (b + c)
and we lack the third property required by
3. âa b c. a * (b - c) = a * b - a * c
Counterexample for 1: a = â, b = 0.
Counterexample for 3: a = â, b = c = 1.
These omissions affect further layers in the type class hierarchy
-- e.g. we cannot use "ordered_cancel_comm_monoid_diff", even
though some of its theorems (e.g. "add_diff_assoc2") turn out to
My proposal is to change the definition of subtraction so that "â -
â = 0" and to instantiate the missing type classes. I believe this
would make "enat" much less painful to use, and mathematically I'm
not so convinced that "â - â = â" is such a great idea anyway.
Indeed, I have recently implemented ordinals below Î_0 in Isabelle
and was able to have much better automation than with "enat", and
there we have Ï - Ï = 0.
"enat" occurs in about 70 ".thy" files in Isabelle and the AFP, so
this change (including the type class instantiations) seems quite
manageable. We (= Mathias and I) would wait until after the 2016-1
release to avoid any interference.
Any opinions for or against?
This archive was generated by a fusion of
Pipermail (Mailman edition) and