[isabelle-dev] "canonical" left-fold combinator for lists

[Florian Haftmann]

>>> The movement of the code setup for sets into the HOL-Main corpus also
>>> brought this fold into List.thy.
>>
>> The task of introducing 'a set as type constructor was, as I still deem,
>> too ambitious to depend on such a detail as the introduction of an
>> additional definition into List.thy.
> 
> The irony is: if you had just added fold to List, without modifying
> foldl/r, it would have been less work for you and we could have
> discussed the unfication of the folds afterwards.

What is the meaning of »modify« here?  They are still the same.  The
change of the definition of foldl/foldr was a simple device to get
correspondences between them and fold in particular;  choosing *one*
provisory proposal how to bootstrap them was simpler and faster (i.e.
the »modification« created »less work«) than building an abstraction
layer over two or three different developments.  Choosing another
bootstrap is still possible (if not easier than before) and can happen
within a few minutes.

Details and workload of big engineering tasks are hard to foresee
anyway.  Maybe in the future I would use something like
http://live.gnome.org/ProjectHamster ?

Again: personally I have no preference how to fold best, but I guess it
is hard to write theorems like union_set_fold with a different argument
order than that of what is now fold and foldr.  I'm not reluctant to
adjust the whole matter as soon as a coherent proposal is made.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120218/9b4b035d/attachment.sig>