[isabelle-dev] Some proposed extensions to the Isabelle library

[Tobias Nipkow]

Am 21/09/2013 03:08, schrieb Alessandro Coglio:
> Hello,
> 
> The attached file contains a fairly heterogeneous collection of potential
> extensions to the Isabelle library, which I've been developing as part of some
> projects that I'm working on. I think that other Isabelle users may find them
> useful.


Thank you for your lemmas.

I found

lemma finite_number_of_maps_with_finite_domain_and_finite_range:
"finite A ==> finite {m::'a \<rightharpoonup> ('b::finite). dom m = A}"

useful and included it in this more general form

lemma finite_set_of_finite_maps:
assumes "finite A" "finite B"
shows  "finite {m. dom m = A \<and> ran m \<subseteq> B}"

with a proof via the finitness of the set of graphs.

I decided against the list ones merely because they are short and easy but will
look at the while_option ones.

Other people should move other lemmas they find interesting.

Thanks again
Tobias

> Please let me know if you'd rather receive these in smaller chunks, if anything
> needs more explanations, if anything should be changed to conform to Isabelle
> library styles/conventions, etc.
> 
> I also have a general question about library vs. AFP. There seem to be clear
> cases of things that should go into the library (e.g. new theorems on lists or
> sets) and clear cases of things that should go into the AFP (e.g. a theory of
> context-free grammars). But some cases are less clear to me; for example, while
> lattices are in the library, I noticed that categories are in the AFP (well,
> categories are used much less frequently than lattices, so perhaps that's a
> criterion). More concretely, I've been working on a couple of developments
> (/not/ included in the attached file) that I can imagine going into either place:
> 
>   * A theory of indexed products, modeled via maps and also modeled via functions.
>   * A theory of ranges over orders/lattices, part of which use the indexed
>     products mentioned above.
> 
> Does anybody have any guidance? Out of curiosity, have theories ever moved
> between library and AFP, in either direction?
> 
> Thank you in advance and best regards.
> 
> 
> 
> 
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>