Email Gateway (Aug 18 2022 at 18:17): Email Gateway (Aug 18 2022 at 18:17):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
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"
using assms
proof (induct xs)
case Nil thus ?case by auto
next
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
qed
So, one might consider to replace the current lemma list_size_pointwise
by the stronger version list_size_pointwise'.
Cheers,
René
Email Gateway (Aug 18 2022 at 18:17):From: Lawrence Paulson <lp15@cam.ac.uk>
I agree. The current version is unnecessarily week.
Larry Paulson
Email Gateway (Aug 18 2022 at 18:18):From: Lukas Bulwahn <bulwahn@in.tum.de>
Is anyone already changing this to the stronger version right now?
Otherwise I would tackle this change this evening, in two hours from now.
Lukas
Email Gateway (Aug 18 2022 at 18:18):From: Lukas Bulwahn <bulwahn@in.tum.de>
changesets f3635643a376 and fd520fa2fb09 are the result of this thread.
Lukas
Last updated: Apr 24 2024 at 20:16 UTC