Re: [isabelle] list_size_pointwise

changesets f3635643a376 and fd520fa2fb09 are the result of this thread.


On 08/30/2011 04:57 PM, Lukas Bulwahn wrote:
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.
Larry Paulson

On 30 Aug 2011, at 10:44, René Thiemann wrote:

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
  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
Computational Logic Group
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck

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