Email Gateway (Aug 23 2022 at 08:17): Email Gateway (Aug 23 2022 at 08:17):From: Makarius <makarius@sketis.net>
Maybe, but it will require substantial work. I've put it onto the new formal
Wishlist:
https://isabelle-dev.sketis.net/T14
https://isabelle-dev.sketis.net/maniphest/query/all
Note that this is not a public "issue tracker", but a curated collection of
well-defined open questions to be addressed in the short/medium/long term.
Makarius
Email Gateway (Aug 23 2022 at 08:30):From: Randy Pollack <rpollack@inf.ed.ac.uk>
A few feature requests:
Add "remark" to the initial goal commands "lemma", "theorem", etc.
This would be useful when formalizing articles or books, to help
readers follow how the formalization matches the document.
Add "type_synonym" to locale specifications and Isar commands that
accept a locale target. For example
type_synonym atm = "int * 'a". (* where 'a is locally
bound in the locale *)
is currently not possible anywhere in a locale specification or in the
body of a context. In 2013 Makarius wrote:
======================
It is in principle possible to support that, but adding even more
infrastructure to local context. The localized version of type_synonym
in Isabelle2013 is still a bit crude in that respect. I did not push
this further so far, because so many other tools that introduce types
are not fully localized yet and need to catch up with the advances
from 2009/2010.
===============
Can this feature be supported now?
Thanks,
--Randy
Email Gateway (Aug 23 2022 at 08:31):From: Makarius <makarius@sketis.net>
There are already many possibilities for formal comments or markers. It
depends what exactly you want to do with them, apart from just citing a
website or bibtex item.
Here are some examples for formal comments with antiquotations:
theory Scratch
imports Main
begin
lemma "((P ⟶ Q) ⟶ P) ⟶ P"
― ‹Peirce's Law›
― ‹see also 🌐‹https://ncatlab.org/nlab/show/Peirce's+law››
proof
assume *: "(P ⟶ Q) ⟶ P"
show P
proof (rule classical)
― ‹key rule of classical logic›
― ‹see also 🌐‹https://ncatlab.org/nlab/show/classical+logic››
assume "¬ P"
have "P ⟶ Q"
proof
assume P
with ‹¬ P› show Q ..
qed
with * show P ..
qed
qed
end
Input works by completing the template "\co" in Isabelle/jEdit.
Starting with Isabelle2019 there is also a formal "marker" concept attached to
individual commands. There are some predefined marker elements based on
"Dublin Core Metadata". For example:
lemma ... ✐‹description ‹Peirce's Law››
You can place the marker everywhere in the command span.
To explore the formal marker space, the normal PIDE technology helps: ✐‹__›
will cause an error that contains completion information.
It is easy to define new markers in user space: this is comparable to
attribute definitions.
We only need good proposals for formal markers, and good catalogs of
mathematical concepts etc. to refer to.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC