Re: [isabelle] arith on large modulus
Ok, thanks for looking into this, Amine.
On Jul 19, 2008, at 1:34 AM, Amine Chaieb wrote:
There is a problem converting this goal into a goal over int. The
new goal after conversion still contains nat and int, which which
the core presburger tactic can not cope. We need a more clever
conversion, which takes numerals into account, which occur in a
statement containing both nat and int with explicit conversions (nat
This could be more involved than the actual approach, an I think we
can not come around a specialized procedure -- i.e. a conversion or
a set of simprocs + rules.
PS: We could think about adding some intro rules to presburger if
such statements occur often. Candidates are mod_pos_pos_trivial and
mod_less and others, to prove that some modulo operations are
basically the same as the usual operations assuming that the input
is within the size of the modulus.
Tobias Nipkow wrote:
It appears there is a bug. Which is not so easy do diagnose :-(
John Matthews schrieb:
I would like to automatically prove the following lemma:
"[|\<not> 100 < nat (x); 0 \<le> x|]
==> nat x + 11 = nat ((x + 11) mod 4294967296)"
I thought this fell within the fragment that arith can handle, but
it can't seem to prove it. I know how to prove this manually, but
is there something else I can use to prove it in a single command?
This archive was generated by a fusion of
Pipermail (Mailman edition) and