Re: [isabelle] list_size_pointwise
Is anyone already changing this to the stronger version right now?
Otherwise I would tackle this change this evening, in two hours from now.
On 08/30/2011 11:52 AM, Lawrence Paulson wrote:
I agree. The current version is unnecessarily week.
On 30 Aug 2011, at 10:44, René Thiemann wrote:
when looking at the thm in Libary List
lemma list_size_pointwise: assumes "!! x. x : set xs ==> f x< g x"
shows "list_size f xs<= list_size g xs"
I was wondering why the strict inequality is used in the assumption. Indeed,
the lemma also holds in its stronger version where only<= is used in the assumption.
lemma list_size_pointwise': assumes "\<And> x. x \<in> set xs \<Longrightarrow> f x \<le> g x"
shows "list_size f xs \<le> list_size g xs"
proof (induct xs)
case Nil thus ?case by auto
case (Cons x xs)
have "list_size f xs \<le> list_size g xs"
by (rule Cons(1), insert Cons(2), auto)
with Cons(2)[of x]
show ?case by auto
So, one might consider to replace the current lemma list_size_pointwise
by the stronger version list_size_pointwise'.
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck
This archive was generated by a fusion of
Pipermail (Mailman edition) and