# Re: [isabelle] arith tactic

`Hi Rafal, thanks for the lemma. My understanding is that the arith
``tactic is able to handle the mod operator, provided that its second
``argument is a constant. In fact, after I sent off my original email,
``I was able to get arith to prove the lemma, with a bit of manual
``guidance:
`
lemma arith_example:
"[|(i::int) < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < (i + 1) mod 256"
apply (subst mod_pos_pos_trivial, auto)
by arith
In that proof script, this is the subgoal given to arith to solve:
"[|i < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < 255"

`The arith tactic still needed to have understood the mod operator to
``have solved this subgoal.
`

`The bigger issue is that we'll be encountering many, many subgoals
``like this in our projects here, most of which involve reasoning about
``machine arithmetic. So we're relying on arith to discharge them
``automatically and efficiently.
`
All the best,
-john
On Feb 14, 2006, at 11:06 PM, Rafal Kolanski wrote:

`Should arith be able to pull this off? It looks like it's missing
``the ability to reason when "k mod n = k", even given the obvious. I
``was distracted and made this, it may be of some use to you:
`
lemma arith_example:
assumes
a: "(i::int) < (nb - 1) mod 256"
"0 <= nb"
"nb < 256"
"0 <= i"
"i < 256"
shows "i < (i + 1) mod 256"
proof -
{
assume c: "nb = 0"
with a have "(i + 1) mod 256 = i + 1"
by (subst mod_pos_pos_trivial) auto
hence ?thesis by simp
}
moreover {
assume c: "nb \<noteq> 0"
with a have lim1: "nb - 1 \<ge> 0" by simp
with a have "nb - 1 < 256" by simp
with lim1 have "(nb - 1) mod 256 = nb - 1"
by (subst mod_pos_pos_trivial) auto
with a lim1 have ?thesis
by (subst mod_pos_pos_trivial) auto
}
ultimately show ?thesis by (cases, auto)
qed
Regards,
Rafal Kolanski.
John Matthews wrote:

`Hi, I've run into a problem using the arith tactic. I ran arith
``for over 15 minutes on the following subgoal, without success:
`lemma arith_example:
"[|(i::int) < (nb - 1) mod 256;
0 <= nb;
nb < 256;
0 <= i;
i < 256|]
==> i < (i + 1) mod 256"
apply arith
I'm running the Isabelle_08-Feb-2006 snapshot.
Thanks,
-john

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*