Re: [isabelle] Proving with Indexed Sums



Am Dienstag, den 11.12.2012, 10:49 -0200 schrieb Alfio Martini:
> Dear  Isabelle Users,
> 
> I wonder if there is a better way to express the summations below in
> Isabelle/HOL/Isar (I might think there is).

I assume you want to try different ways to write down your lemma. If you
just need Gauss summation there are a couple of lemmas in Set_Interval
(gauss_sum and arith_sums_general), just use
  find_theorems setsum "_ * _"  .

> In particular, I do not get why the first two theorems express the subgoals
> in term of the "lowest" level
> terms "setsum" and "op" while the third one thankfully not.

First "∑j=0..n. 2*j" is just a different syntax for "∑j∈{0..n}. 2*j" the
proof methods in Isabelle do not see any difference. So sum_pattern01
and sum_pattern02 are exactly the same theorems.

What is the difference between sum_pattern02 and sum_pattern03:

Isabelle applies eta normalization before it stores/displays terms
  "%x. f x" is rewritten to f

so "SUM j : A. 2 * j"
	-display->
  "setsum A (%j. 2 * j)"
	-eta->
  "setsum A (op * 2)"
there is no syntax defined for the last term so it is displayed as is.
For sum_pattern03 eta normalization does not change the term.

> Especially, I
> don´t see any "relevant" difference
> between sum_patter02 e sum_pattern03.

  %j. 2 * j  -eta->  op * 2

whereas

  %j. 2 * j + 1   is not eta reducible.

> As a last unrelated question, in theorem sum_pattern04, I could not prove
> the inductive step with either
> simp or auto. When using exponentiations, what kind of proof method does
> one has to usually use?

Isabelle does not automatically unfold "t^2" as t might be a quite big
term. Use simp add: power2_eq_square to solve this.

> Thanks for any help!
> ---------
> theorem sum_pattern01:
>    fixes n::nat
>    shows "(∑j∈{0..n}. 2*j)= n * (n+1)" (is "?P n")
>    proof (induction n)
>     show "?P 0" by simp
>     next
>     fix x0::nat
>     assume "?P x0"
>     from this show "?P (Suc x0)" by simp
>   qed
> 
> theorem sum_pattern02:
>    fixes n::nat
>    shows "(∑j=0..n. 2*j)= n * (n+1)" (is "?P n")
>    proof (induction n)
>     show "?P 0" by simp
>     next
>     fix x0::nat
>     assume "?P x0"
>     from this show "?P (Suc x0)" by simp
>   qed
> 
> theorem sum_pattern03:
>    fixes n::nat
>    shows "(∑j=0..n. 2*j+1) = (n+1) * (n+1)" (is "?P n")
>    proof (induction n)
>      show "?P 0" by simp
>      next
>      fix x0
>      assume IH: "?P x0"
>      from this show "?P (Suc x0)" by simp
>    qed
> 
> theorem sum_pattern04:
>    fixes n::nat
>    shows "(∑j=0..n. 2*j+1) = (n+1)^2" (is "?P n")
>    proof (induction n)
>      show "?P 0" by simp
>      next
>      fix x0
>      assume IH: "?P x0"
>      from this show "?P (Suc x0)" by simp (* fails *)
>    qed







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