*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Extensions to the basic Isabelle/HOL theories*From*: Matthias Daum <md11 at wjpserver.cs.uni-sb.de>*Date*: Wed, 06 May 2009 16:49:55 +0200*User-agent*: Thunderbird 2.0.0.5 (X11/20070727)

Dear list, it seams as if the former list isabelle-lemmas at cl.cam.ac.uk has vanished? If you are still interested in extending the basic Isabelle/HOL theories by lemmata from their users, you might consider to include the following lemmata, which I needed during my work with Isabelle: lemma ex_ivl_less: (EX i:{..<n}. P i) = (EX i<n. P i) and all_ivl_less: (ALL i:{..<n}. P i) = (ALL i<n. P i) by auto lemma distinct_takeWhile: "distinct xs ==> distinct (takeWhile P xs)" proof (induct xs) case (Cons x xs) thus ?case by clarsimp (frule set_take_whileD, clarsimp) qed simp Moreover, the two following lemmata could be incorporated into the library's theory Nat_Infinity: instance inat :: "{linorder}" by intro_classes (auto simp add: inat_defs split: inat_splits) lemma not_Infty_eq: "(x ~= Infty) = (EX i. x = Fin i)" by (cases x) auto Furthermore, I have enclosed a theory for the summation of a list of values. I am not sure, whether you prefer to incorporate the definition and proofs in the basic List theory or store it somewhere at the libraries... Unfortunately, the proofs are checked only in Isabelle/HOL 2005, I hope, they still run through in the newest Isabelle release. Best regards, Matthias. -- Matthias Daum Institut für Rechnerarchitektur und Parallelrechner Universität des Saarlandes Postfach 151150 - D-66041 Saarbrücken Tel.: +49 (0)681 302-64715, Fax: +49 (0)681 302-4290

theory list_sum imports Main begin lemma add_start_foldl_sum: "!!(y::'a::semigroup_add). x + foldl op + y xs = foldl op + (x+y) xs" by (induct xs) (simp_all add: add_assoc) lemma "foldl op + (0::'a::{ab_semigroup_add, zero}) xs = foldr op + xs 0" proof (induct xs) case (Cons x xs) note calculation = this moreover have "0 + x = x + 0" by (rule add_commute) ultimately show ?case by (simp add: add_start_foldl_sum[symmetric]) qed simp constdefs list_sum::"'a list \<Rightarrow> ('a::{zero,plus})" "list_sum xs == foldr op + xs 0" lemma list_sum_Nil[simp]: "list_sum [] = 0" and list_sum_Cons[simp]: "list_sum (x#xs) = x + list_sum xs" by (simp_all add: list_sum_def) lemma distinct_list_sum_set_eq: "distinct xs \<Longrightarrow> list_sum xs = \<Sum>(set xs)" by (induct xs) simp_all lemma list_sum_append: "list_sum (xs at ys) = list_sum (xs::'a::{comm_monoid_add} list) + list_sum ys" by (induct xs) (simp_all add: add_assoc) lemma add_list_sum_take_drop: "n \<le> length (xs::'a::{comm_monoid_add} list) \<Longrightarrow> list_sum (take n xs) + list_sum(drop n xs) = list_sum xs" by (simp add: list_sum_append[symmetric]) lemma list_sum_nat_mono: "n \<le> length (xs::nat list) \<Longrightarrow> list_sum (take n xs) \<le> list_sum xs" by (simp add: add_list_sum_take_drop[symmetric]) end

**Follow-Ups**:**Re: [isabelle] Extensions to the basic Isabelle/HOL theories***From:*Tobias Nipkow

- Previous by Date: [isabelle] A Quantification Binding Question
- Next by Date: Re: [isabelle] Extensions to the basic Isabelle/HOL theories
- Previous by Thread: Re: [isabelle] A Quantification Binding Question
- Next by Thread: Re: [isabelle] Extensions to the basic Isabelle/HOL theories
- Cl-isabelle-users May 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list