[isabelle] Extensions to the basic Isabelle/HOL theories

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

Unfortunately, the proofs are checked only in Isabelle/HOL 2005, I hope,
they still run through in the newest Isabelle release.

Best regards,

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

lemma add_start_foldl_sum:
   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
  have "0 + x = x + 0" by (rule add_commute)
  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"

  list_sum_Nil[simp]:  "list_sum [] = 0"
  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])


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