Re: [isabelle] (i>0) & (int n = i) & P(n) ==> P(i)



Here is a direct proof, without preconditions:

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

Tactic arith cannot deal with it because it contains multiplication in an essential way. However, if you first multiply out, then arith can solve it:

apply(simp add: ring_simps)
apply arith
done

Regards
Tobias


Hauser Bruno wrote:
Hi

I want to prove the following lemma: ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2. Proving the property for naturals succeeds. I now want to proof it for positive, nonzero integers. Trying to solve the lemma (i_equation_int) automatically with sledgehammer did not succeed. So, no "trivial" solution seems to exist yet.

lemma i_equation_int: "[|(n - (1::nat)) * n div 2 + n =  n * (n + 1) div 2; int n = i; i > 0|] ==> ((i - (1::int)) * i div 2) + i = i * (i + 1) div 2"

Can someone give me a hint how to proof it by (maybe) using the facts, that i > 0 and the equation holds for naturals?

Is there a general way for proofing lemmas like: (i>0) & (int n = i) & P(n) ==> P(i) ?

Thank you,
Bruno Hauser





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