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
apply(simp add: ring_simps)
Hauser Bruno wrote:
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) ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and