Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Antiquotations to print existing definitions i...

view this post on Zulip Email Gateway (Aug 22 2022 at 20:40):

From: Martin Desharnais <martin.desharnais@gmail.com>
Dear Isabelle users,

with the document preparation system, it is possible to use
antiquotations such as @{thm a} to print a lemma or @{term t} to print a
term. I could not, however, find a way to print an existing definition.
I am especially interested in datatypes, functions, and locales
definitions. My use case is as follows.

I import external theories and want to write about their definitions.
The only way I could find is to copy-paste said definitions in an
unnamed context and annotate them as private.

(<)
context begin
(>)

text ‹...›

(<) private (>)
datatype 'a option =
None |
Some (the: 'a)

text ‹...›

(<) private (>)
primrec append :: "'a list ⇒ 'a list ⇒ 'a list" (infixr "@" 65) where
append_Nil: "append [] ys = ys" |
append_Cons: "append (x#xs) ys = x # append xs ys"

text ‹...›

(>)
end
(<)

Just printing the simplification theorems @{thm append.simps} is not an
option, because the number of simplification theorems quickly explodes
for functions depending on the linear "first match succeeds" of pattern
matching.

What I would like, is a way to avoid this copy-pasting. Ideally, a
solution would take the form of antiquotations such as @{type_def list},
@{const_def append}, or @{locale_def somelocale}.

  1. Is there any existing way to avoid copy-pasting?
  2. If there currently exists no ways, would such an extension be feasible?

Regards,
Martin Desharnais

Last updated: Apr 20 2024 at 01:05 UTC