Re: [isabelle] arith on large modulus

Ok, thanks for looking into this, Amine.


On Jul 19, 2008, at 1:34 AM, Amine Chaieb wrote:

Hi John,

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 and int).

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 MHonArc.