Re: [isabelle] list_size_pointwise



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
> 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é
> -- 
> 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 MHonArc.