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) ?

Dear Bruno,

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

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