Email Gateway (Aug 18 2022 at 12:29): Email Gateway (Aug 18 2022 at 12:29):From: 游珍 <yucy0405@163.com>
dear,
I'm an Isabelle newbie trying to verify a proof. The statement of the proof involves \<Sum>. I meet some prombles, the following are my proof;
theory sumlist
imports Main List
begin
consts
setn::"nat \<Rightarrow> nat set"
primrec
"setn 0 = {}"
"setn (Suc n) = insert (Suc n) (setn n)"
lemma f: " (\<Sum>i\<in>(setn (Suc j)). i)=(Suc j)+(\<Sum>i\<in>(setn j). i)"
apply auto
apply ?????
The reslut is displayed in the next window
proof (prove): step 1
goal (1 subgoal):
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>?
need help!
thanks in advance!
yucy
Email Gateway (Aug 18 2022 at 12:30):From: Brian Huffman <brianh@cs.pdx.edu>
Quoting 游珍 <yucy0405@163.com>:
At this point in your proof, you need to you can search for relevant
lemmas by typing ctrl-c, ctrl-f, and using the patterns
"\<Sum>_\<in>_. _" or "SUM _:_. _" together with "insert". The lemma
you need is setsum_insert. In fact, setsum_insert is declared as a
simp rule, but it has a couple of side conditions which prevent it
from rewriting automatically.
If you type:
apply (subst setsum_insert)
you get the following subgoals:
goal (3 subgoals):
1. finite (setn j)
2. Suc j \<notin> setn j
3. Suc j + \<Sum>(setn j) = Suc (j + \<Sum>(setn j))
If you prove the first two subgoals as separate lemmas, and declare
them both as [simp] rules, then your lemma f can be proved completely
by auto.
Hope this helps,
Email Gateway (Aug 18 2022 at 12:30):From: Simon Winwood <sjw@cse.unsw.edu.au>
At Wed, 8 Oct 2008 17:01:38 +0800 (CST),
=?gbk?B?087V5A==?= <yucy0405@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
Last updated: May 03 2024 at 12:27 UTC