Re: [isabelle] how to proof some lemmas containing "\<Sum>"?



At Wed, 8 Oct 2008 17:01:38 +0800 (CST),
=?gbk?B?087V5A==?= <yucy0405 at 163.com> wrote:
> 

[...]

> The reslut is displayed in the next window
> proof (prove): step 1
> goal (1 subgoal):
>  1. \<Sum>(insert (Suc j) (setn j)) = Suc (j + \<Sum>(setn j))
>  
> Which method or rule I can choose? How to use these methods and
> rules? I don't known any lemmas and themorems about \<Sum>.How can i
> get some informations about \<Sum>?

  It seems obvious that you need something about \<Sum> and insert.
Isabelle has a very useful find-theorems command (I use it via C-c C-f
in Emacs) --- in this case it is a little tricky as \<Sum> is a
translation for setsum (which I found by greping for \<Sum> in
isabelle/HOL).  If you search for "\<Sum>_._" and insert (or setsum
and insert), you get a number of lemmas from Finite_Set, of which
setsum_insert is the one we want.

  This requires a few helper lemmas, but the proof is more or less
straightforward (especially if you keep in mind that most lemmas to be
proved about setn will be via induction):

theory sumlist
imports Main List
begin

consts
setn::"nat  \<Rightarrow>  nat set"

primrec
"setn 0 = {}"
"setn (Suc n) = insert (Suc n) (setn n)"

lemma finite_setn:
  "finite (setn n)"
  apply (induct n)
   apply simp
  apply simp
  done

lemma setn_n_le_n:
  "x \<in> setn n \<Longrightarrow> x \<le> n"
  apply (induct n)
   apply simp
  apply fastsimp
  done

lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)"
proof (subst setn.simps, rule setsum_insert)
  show "finite (setn j)" by (rule finite_setn)
  
  show "Suc j \<notin> setn j"
  proof
    assume "Suc j \<in> setn j"
    hence "Suc j \<le> j" by (rule setn_n_le_n)
    thus False by simp
  qed
qed

end

	Simon







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