Stream: Beginner Questions

Topic: Haskell like pattern matching "@" operator

Bob Rubbens (Apr 29 2023 at 08:08):

Good morning everyone, in haskell one can use the "@" to declare a variable for a variable that was pattern matched on. For example, one can have ps@(p:pt), meaning, the entire list ps has head p and tail pt. Is there something like this in isabelle?

Adem Rimpapa (Apr 29 2023 at 11:32):

I believe what you're looking for can be found in the theory HOL-Library.Pattern_Aliases. If you import this theory, you can use the syntax (p # pt =: ps), for example as follows:

context
includes pattern_aliases
begin

fun f :: "'a list ⇒ 'a list" where
  "f [] = []" |
  "f (p # pt =: ps) = ps"

end

Bob Rubbens (Apr 29 2023 at 14:43):

That's great! Looks like that's exactly what I need. Thanks a bunch.

If you don't mind a follow-up question: this just happened to be included somehow with my isabelle installation. By ctrl+clicking on the import statement I could look into the source and hence the (inline comment) docs. On the internet I also found a nicely formatted PDF. Do you know if this PDF does also happen to be in my isabelle installation? I have the prog-prove.pdf, locales.pdf, etc. in the jedit documentation pane, but there seems to be no PDF on HOL-Library/Pattern_Aliases. I also browsed around my isabelle folder and indeed the number of pdfs seems limited. Is there some extra pdf documentation package I can download? Or can I maybe render these PDFs myself locally?

Adem Rimpapa (May 01 2023 at 13:10):

A simple way to just generate the pdf for a given session (for example HOL-Library, which contains the Pattern_Aliases theory) is to run the following on your command line:

isabelle document -v -V -P /path/to/some/directory HOL-Library

This will generate the pdf file for the session HOL-Libraryin the specified directory. You can find more detailed descriptions of Isabelle's document generation functionality in the Isabelle system manual (https://isabelle.in.tum.de/dist/Isabelle2022/doc/system.pdf), mainly in chapter 3.

Bob Rubbens (May 02 2023 at 06:36):

Oh cool! Thanks!

Last updated: Apr 27 2024 at 20:14 UTC