Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)
Hauser Bruno wrote:
Is there a general way for proofing lemmas like: (i>0) & (int n = i)
& P(n) ==> P(i) ?
The answer is "yes" and "no." There are methods for transferring results
from the natural numbers to the integers and vice-versa, though they are
Suppose you have a theorem of the form "ALL (n::nat). P n" and you want
a theorem of the form "ALL i >= (0::int). P' i", where P' is the
translation of P to the integers (e.g. nat functions and relations like
+, div, < are replaced by the integer versions).
First, use a general rule to convert "ALL i >= (0::int). P' i" to "ALL
n. P' (int n)." Then using simplification rules like
int n + int m = int (n + m)
(int n) div (int m) = int (n div m)
int n < int m = n < m
and magically "ALL n. P'(int n)" is transformed to "ALL n. P n," which
is what you have already proved. Amine Chaieb once described a similar
method on this mailing list.
(Your question involved proving, more simply, P'(int n) from P n, which
only needs the simplification rules.)
I have been revising the number theory libraries and using this method
to make sure that all basic theorems are in place for both nats and
ints. If you want, I can send you a file that works in the developer
version of Isabelle, which uses the method above to transfer results
involving gcd, lcm, factorial, prime, congruence, choose, and fib. But
it is still tedious. Chaieb and I have been working on better ways of
automating the procedure, and hope to have better methods soon.
This archive was generated by a fusion of
Pipermail (Mailman edition) and