[isabelle-dev] [isabelle] Suggestions for src/HOL/Fun.thy

[Lawrence Paulson]

The new proposed lemmas look useful but a little arbitrary. For example, one can imagine multiplicative versions of most of them as equally justifiable and useful.

It makes sense to remove needless restrictions from material we already have and then to fill any obvious gaps in the material, but we do need a way of stopping.

Tobias’s suggestion of a new theory is helpful especially if it arrives later in the build process. Note that presburger is not actually available in Fun.thy.

Larry

> On 9 Oct 2022, at 06:34, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> I did not add any of your additional lemmas (see 3 below) to Fun.thy because I wonder whether Fun.thy is the best place for them: they are purely algebraic, but on a functional level. Originally Fun.thy was meant to hold very generic lemmas about functions, eg intjectivity, surjectivity etc. Then monotonicity reasoning. Then more algebraic lemmas crept in, eg "surj ((+) a)", which prompted you to suggest further algebraic lemmas.
> 
> The reason for this is that at the point where all the order and algebra type classes are defined, Fun.thy (with o, inj, surj etc) is not known yet. The reason is that Fun builds on Set which uses boolean_algebra which uses Lattices which uses Groups.
> 
> General question: should we continue to put material that morally belongs into algebra into Fun (and improve its section structure) or should we start a new theory?
>