Re: [isabelle] Extensions to the basic Isabelle/HOL theories



Many thanks for your input, I have already moved half your lemmas into
the distribution. You seem to be the only one who provides new lemmas.
Hence we removed isabelle-lemmas at cl.cam.ac.uk - it may even have
attracted spam, I cannot remember. If other people suddenly feel
motivated to provide additional lemmas and there is too much of it on
this list, this would motivate us to think again about new ways of
integrating your contributions.

Tobias
PS I'll let you know separately what I added and how.

Matthias Daum schrieb:
> 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.
> 





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