[isabelle] Proving with Indexed Sums



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

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. Especially, I
don´t see any "relevant" difference
between sum_patter02 e sum_pattern03.

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?

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
-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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