[isabelle-dev] NEWS: Pattern Aliases

[Lars Hupel]

* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
for pattern aliases as known from Haskell, Scala and ML.


This is a small library theory providing convenient syntax for defining
recursive functions. Tobias is already using this for defining functions
over trees. For example:

function merge :: "('a::linorder) heap ⇒ 'a heap ⇒ 'a heap" where
"merge Leaf h = h" |
"merge h Leaf = h" |
"merge (Node l1 a1 r1 =: h1) (Node l2 a2 r2 =: h2) =
   (if a1 ≤ a2 then Node (merge h2 r1) a1 l1
    else Node (merge h1 r2) a2 l2)"

Users of Haskell or Scala should be familiar with this syntax (both use
"@" instead of "=:", but "@" is already used in HOL).

To use this syntax, you need to import "HOL-Library.Pattern_Aliases" and
activate the bundle "pattern_aliases" either locally or globally. I
recommend doing this only locally, i.e.

context includes pattern_aliases begin

(* ... *)

end

This avoids polluting the global syntax.

Some more documentation can be found in the theory file.

There is still time to tweak this for the 2017 release, so comments are
welcome.

Cheers
Lars