[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
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



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