Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proofs involving Integers

Email Gateway (Aug 18 2022 at 11:49):

From: George Karabotsos <g_karab@cs.concordia.ca>
Hello,

I am having trouble proving the following lemmas that involve integers.
For example, the following:

lemma "-(x * (i + (1::int))) = - ((x * i)+x)"

or

lemma "- (x * (i + (1::int))) + x = - (x * i)"

I was looking for a distribution rule for mult. and add. to try to
simplify these lemmas but I was not able to locate something appropriate.

Any help is appreciated.

TIA

George

Email Gateway (Aug 18 2022 at 11:50):

From: Tobias Nipkow <nipkow@in.tum.de>
If you are looking for a theorem involving a specific pattern, press the
big "Find" button, type in the pattern (in this case "_*(_+_)" or
something similar), hit return, and admire the result: a list which will
include your desired theorem, should it exist. In your case: int_distrib
(from theory.... Int!)

Tobias

George Karabotsos schrieb:

Email Gateway (Aug 18 2022 at 11:52):

From: Amine Chaieb <chaieb@in.tum.de>
Hi,

These are simple instances of simple rewriting with AC, so simp add:
ring_simps would do the job. For more complicated instances including
only equality and disequality (~=) try the algebra method.

Amine.

George Karabotsos wrote:

Last updated: May 03 2024 at 08:18 UTC