[Club2] Talk by Lorenz Panny: Primitively (co)recursive function definitions for Isabelle/HOL

[Johannes Hölzl]

Greetings,

On Wednesday, Aug. 14, Lorenz Panny will present his B.Sc. thesis to the
group (supervised by Dmitriy and Jasmin). This is a repeat of the talk
he held at the Isabelle Workshop in Vienna, for the benefit of those of
you who couldn't attend.

Primitively (co)recursive function definitions for Isabelle/HOL
Lorenz Panny
Wed., Aug. 14, 14:00, Room: Turing (00.09.038)

Isabelle/HOL has lately been extended with a definitional package
supporting modular (co)datatypes based on category theoretical
constructions. The implementation generates the specified types and
associated theorems and constants, notably (co)recursors, but initially,
there was no convenient way of specifying functions over these types.
This thesis introduces the high-level commands primrec, primcorec and
primcorecursive that can be used to define primitively (co)recursive
functions over Isabelle’s new (co)datatypes using an intuitive syntax.
Automating a tedious process, a user specification is internally reduced
to a (co)recursor-based definition. Using the (co)recursor theorems, it
is then proved and introduced as theorems that the definition does in
fact fulfill the specified properties.

--

Cheers, 
  Johannes