[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

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.


Scrap your boilerplate!
And enjoy.

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