Re: [isabelle] Proofs involving Integers
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!)
George Karabotsos schrieb:
I am having trouble proving the following lemmas that involve integers.
For example, the following:
lemma "-(x * (i + (1::int))) = - ((x * i)+x)"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and