Email Gateway (Nov 29 2024 at 09:30): Email Gateway (Nov 29 2024 at 09:30):From: "\"Putti, Edoardo (UT-EEMCS)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle users,
I'm tutoring students in a master course. One of the learning objectives for this week was finding theorems.
Because of the syntax translations it's hard for them to go from a term such as "{1, 2, 3}" to
"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use find_theorems to get unstuck.
*
Is there an option to "turn off" syntax?
*
Is there a way to get all syntax translations involved in a term parsing/unparsing?
*
Is there a way to go to the syntax rules definition?
Email Gateway (Nov 29 2024 at 14:41):From: i n <cl-isabelle-users@lists.cam.ac.uk>
Hi, Im pretty sure you should be able to use this
no_translations
"{x, xs}" ⇌ "CONST insert x {xs}"
"{x}" ⇌ "CONST insert x {}"
no_syntax
"_Finset" :: "args ⇒ 'a set" ("{(_)}")
Bundles don't support translations so you cant really use bundles. You have to remove the translation before removing the syntax. (This feature should be supported if any isabelle developer sees this)
Also you need to ensure all your theories are based of this and you do not have another theory that imports Main or HOL.* directly without this or you will get the set syntax back due to the import.
Cheers,
Irvin
On Friday, 29 November 2024 at 09:30:42 am UTC, \"Putti, Edoardo (UT-EEMCS)\"" (via cl-isabelle-users Mailing List) <cl-isabelle-users@lists.cam.ac.uk> wrote:
#yiv2145379254 P {margin-top:0;margin-bottom:0;}Dear Isabelle users,
I'm tutoring students in a master course. One of the learning objectives for this week was finding theorems.
Because of the syntax translations it's hard for them to go from a term such as "{1, 2, 3}" to"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use find_theorems to get unstuck.
- Is there an option to "turn off" syntax?
- Is there a way to get all syntax translations involved in a term parsing/unparsing?
- Is there a way to go to the syntax rules definition?
Email Gateway (Dec 01 2024 at 14:47):From: Makarius <makarius@sketis.net>
On 29/11/2024 10:30, "Putti, Edoardo (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
I'm tutoring students in a master course. One of the learning objectives for
this week was finding theorems.Because of the syntax translations it's hard for them to go from a term such
as "{1, 2, 3}" to
"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use
find_theorems to get unstuck.
Note that Isabelle2025 (March 2025) will have a lot of extra markup, both in
the input and output of the term language. Thus you can hover over the curly
braces above to get to the underlying constant "Set.insert". Moreover,
inner-syntax blocks will be highlighted, together with semi-formal comments
about their purpose: above that is 'notation: mixfix "set enumeration"' --- it
is up to the library to defined that for mixfix, while infix and binder are
automatic.
You can try it e.g. with current Isabelle/e8b388c2b490 or a snapshot from
https://isatest.sketis.net/devel/release_snapshot
Note that the release schedule is here
https://isabelle-dev.sketis.net/phame/post/view/77/plan_for_isabelle2025_release
* Is there an option to "turn off" syntax?
You can approximate that in Isabelle/ML as follows, but the result contains a
lot of extra details:
ML ‹@{term ‹{1, 2, 3}›}›
* Is there a way to get all syntax translations involved in a term parsing/
unparsing?
See the command 'print_syntax', but the result contains a lot of extra details.
* Is there a way to go to the syntax rules definition?
There is no direct way for that, only indirectly because the formal link e.g.
to constant "Set.insert" gets you where the translations are also defined.
(The reason for the lack of links for 'syntax' and 'translations' is that
these have no formal status; there is just one big bucket of unscoped/untyped
things.)
Instead of showing too much low-level things, I would rather teach beginners
to work with PIDE markup, both in the input buffer or output panel.
Makarius
Email Gateway (Feb 03 2025 at 21:59):From: Makarius <makarius@sketis.net>
On 29/11/2024 10:30, "Putti, Edoardo (UT-EEMCS)" (via cl-isabelle-users
Mailing List) wrote:
Dear Isabelle users,
I'm tutoring students in a master course. One of the learning objectives for
this week was finding theorems.Because of the syntax translations it's hard for them to go from a term such
as "{1, 2, 3}" to
"insert 1 (insert 2 (insert 3 bot)))" in their head and therefore actually use
find_theorems to get unstuck.*
Is there an option to "turn off" syntax?
*
Is there a way to get all syntax translations involved in a term parsing/
unparsing?
*
Is there a way to go to the syntax rules definition?
Hi Edoardo,
maybe you want to check the situation in Isabelle2025-RC1. The NEWS section on
"Inner syntax --- the term language" has a lot of details and fine points. The
big picture probably needs to be explored experimentally: we have now a quite
different situation for term syntax, many decades after its initial introduction.
Your question about "turn off syntax" is answered by the many syntax bundles
that are now in the library. Here is an example for set enumeration:
notepad
begin
let ?test = "{x, y, z}"
include no set_enumeration_syntax
term ?test
end
Note that in a context that includes no set_enumeration_syntax, there is no
way to read that notation, which explains my auxiliary term abbreviation ?test
above: first read with syntax, then print without syntax.
I would normally explore the substructure of terms more directly via
C-hover-mouse (or only hover-mouse in Output). This provides a lot of clues,
without suppressing notation. There are also new hyperlinks, e.g. from the { }
braces to Set.insert.
Makarius
Email Gateway (Feb 03 2025 at 22:02):From: Makarius <makarius@sketis.net>
On 29/11/2024 15:40, i n (via cl-isabelle-users Mailing List) wrote:
Bundles don't support translations so you cant really use bundles. You have to
remove the translation before removing the syntax. (*This feature should be
supported if any isabelle developer sees this*)
I have "localized" syntax translations for Isabelle2025-RC1. Note that there
are many other changes to inner syntax in the forthcoming release. So old
problems need to be matched against new possibilities in a quite different system.
Makarius
Last updated: Feb 05 2025 at 16:23 UTC