[isabelle] New AFP entry: Generating linear orders for datatypes



by René Thiemann

We provide a tactic which automatically synthesizes linear orders for datatypes
as it is possible using Haskell's ``deriving Ord'' feature. The tactic is able
to handle datatypes with mutual or higher-order recursion, if the nesting is not
too complex.

Our method complements the Isabelle Collection Framework which for some
datastructures---like balanced trees---demands that the type of keys is linearly
ordered.

Our formalization was performed as part of the IsaFoR/CeTA project. With our new
tactic we could completely remove tedious proofs for linear orders of two datatypes.

http://afp.sourceforge.net/entries/Datatype_Order_Generator.shtml

Scrap your boilerplate!
And enjoy.





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