Email Gateway (Aug 19 2022 at 09:56): Email Gateway (Aug 19 2022 at 09:56):From: Joachim Breitner <breitner@kit.edu>
Dear Isabelle users,
I am adding finishing touches to an upcoming AFP entry and I am playing
around a bit with Isabelle’s document generation features. It works
nicely, but I have some questions:
I’d like to use @{term_type foo} on expressions whose type contains a
type synonym, but the result contains the unfolded type. Is there a
better work-around than using
@{term "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}@{text "::"}@{typ "heap ⇒ (exp ⇒ Value) ⇒ Env"}
instead of just
@{term_type "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}
Also, I have trouble with no_document. My ROOT.ML reads
$ cat isa-launchbury/ROOT.ML
no_document use_thys ["/src/HOL/Library/FuncSet", "/src/HOL/Library/LaTeXsugar"];
use_thys ["Everything"];
And indeed, the generated files FuncSet.tex and LaTeXsugar.tex are
empty. But they are included in the session_graph.pdf file. Is there a
way to avoid that?
The next items are more feature suggestions than question, but still:
@{abbrev ..} is nice. Can we have an @{type_abbrev ..} that
pretty-prints the type equations?
Sometimes the lemmas would be clearer if free variables were explicitly
all-quantified. Is there an easy way to achieve this (besides defining a
variant of the lemma with an HOL-∀ in front)?
Breaking a lemma apart with (prem 1), (prem 2) and (concl) to insert it
into the text appropriately is also nice, but feels a bit dangerous –
what if I later change the theory and add a premise. How about a command
that asserts that a certain lemma has exactly n premises that would fail
if that is no longer true? Then the careful author could use the command
near places where he uses (prem 1), (prem 2) and (concl) and be sure
that he presents the lemma fully.
I also miss good ways to automatically print data type definitions. My
work around is to show
lemma Terms:
"∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
by (metis Terms.exp_assn.exhaust(1))
and pretty-print this lemma in the text, but a tool that formats an
exhaust-lemma in the style of a grammar specification would be slick.
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 09:56):From: Tobias Nipkow <nipkow@in.tum.de>
Not that I know. The original type is lost, so you have to write at least one
type, but to avoid writing two types you would need some ML (to check that the
type you give is the right one).
Tobias
Email Gateway (Aug 19 2022 at 09:56):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joachim,
I’d like to use @{term_type foo} on expressions whose type contains a
type synonym, but the result contains the unfolded type. Is there a
better work-around than using
@{term "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}@{text "::"}@{typ "heap ⇒ (exp ⇒ Value) ⇒ Env"}
instead of just
@{term_type "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}
I would suggest @{term_type [source] "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒
Env"}
@{abbrev ..} is nice. Can we have an @{type_abbrev ..} that
pretty-prints the type equations?
Something to think about.
Sometimes the lemmas would be clearer if free variables were explicitly
all-quantified. Is there an easy way to achieve this (besides defining a
variant of the lemma with an HOL-∀ in front)?
You could write a style in ML for the term antiquotation to add the
quantifiers to propositions. See the LaTeX sugar document for
fundamental hints, or just get back here.
I also miss good ways to automatically print data type definitions. My
work around is to show
lemma Terms:
"∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
by (metis Terms.exp_assn.exhaust(1))
and pretty-print this lemma in the text, but a tool that formats an
exhaust-lemma in the style of a grammar specification would be slick.
Maybe also something which can be implemented as term style, e.g.
expecting an exhaustivness lemma as produced by datatype and rearranging
it as desired.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 09:56):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Joachim,
I’d like to use @{term_type foo} on expressions whose type contains a
type synonym, but the result contains the unfolded type. Is there a
better work-around than using
@{term "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}@{text
"::"}@{typ "heap ⇒ (exp ⇒ Value) ⇒ Env"}
instead of just
@{term_type "heapToEnv:: heap ⇒ (exp ⇒ Value) ⇒ Env"}
type_synonym declarations only introduce the parse translations for type
abbreviations. The print direction like for term abbreviations is not
produced automatically, but you can add it manually:
translations (latex)
(type) heap <= (type) "(var * expr) list"
However, this translation will be applied to all printed type in the
given print mode (latex in the example), so any occurrence of (var *
expr) list" will be printed as "heap". This is similar to printing
abbreviations on the term level. With this translation in place,
@{term_type "heapToEnv :: heap => (exp => Value) => Env"} should print
what you expect.
Also, I have trouble with no_document. My ROOT.ML reads
$ cat isa-launchbury/ROOT.ML
no_document use_thys ["/src/HOL/Library/FuncSet", "/src/HOL/Library/LaTeXsugar"];
use_thys ["Everything"];
And indeed, the generated files FuncSet.tex and LaTeXsugar.tex are
empty. But they are included in the session_graph.pdf file. Is there a
way to avoid that?
I know one way to avoid that: Build a heap image with all auxiliary
theories that you do not want to show up in session_graph.pdf, i.e., HOL
with FuncSet and LaTeXsugar, and then base your session on this image.
I also miss good ways to automatically print data type definitions. My
work around is to show
lemma Terms:
"∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
by (metis Terms.exp_assn.exhaust(1))
and pretty-print this lemma in the text, but a tool that formats an
exhaust-lemma in the style of a grammar specification would be slick.
You don't have to state and prove this lemma yourself, the datatype
package generates a similar one called expr.nchotomy for type expr.
Andreas
Email Gateway (Aug 19 2022 at 09:56):From: Joachim Breitner <breitner@kit.edu>
Hi,
Am Donnerstag, den 17.01.2013, 11:21 +0100 schrieb Andreas Lochbihler:
Also, I have trouble with no_document. My ROOT.ML reads
$ cat isa-launchbury/ROOT.ML
no_document use_thys ["/src/HOL/Library/FuncSet", "/src/HOL/Library/LaTeXsugar"];
use_thys ["Everything"];
And indeed, the generated files FuncSet.tex and LaTeXsugar.tex are
empty. But they are included in the session_graph.pdf file. Is there a
way to avoid that?
I know one way to avoid that: Build a heap image with all auxiliary
theories that you do not want to show up in session_graph.pdf, i.e., HOL
with FuncSet and LaTeXsugar, and then base your session on this image.
Or, in my case, HOL+HOLCF+Nominal2+FuncSet+LaTeXsugar. This leads to
another question:
What should a IsaMakefile look like that uses a custom heap (in my case,
HOL+HOLCF+Nominal2 where Nominal2 comes with my submission in a
subdirectory) so that it works on the AFP?
Also, one of the theories that I want to exclude from the session graph
is Everything, which is actually the part of the introduction that uses
all this pretty-printing, but not really part of the theory. I guess the
heap building does not work here, because the theory is at the very
bottom of the graph?
I also miss good ways to automatically print data type definitions. My
work around is to show
lemma Terms:
"∃ x assn e'. (e = (Lam [x]. e') ∨ (e = Var x) ∨ (e = App e' x) ∨ (e = Let assn e'))"
by (metis Terms.exp_assn.exhaust(1))
and pretty-print this lemma in the text, but a tool that formats an
exhaust-lemma in the style of a grammar specification would be slick.
You don't have to state and prove this lemma yourself, the datatype
package generates a similar one called expr.nchotomy for type expr.
Thanks for the pointer. It seems that nominal_datatye does not build
such a lemma. Also, I had to collect all existentially quantified
variables in the front so that the lemma would fit on one line :-)
Greetings,
Joachin
signature.asc
Email Gateway (Aug 19 2022 at 09:57):From: Joachim Breitner <breitner@kit.edu>
Hi,
I tried to do it using the translation and syntax features, and here is
what I cam up with, based on my very partial understanding of these
features:
abbreviation (Grammar output)
"grammar_imp"
where
"grammar_imp ≡ op ⟶"
syntax (Grammar output)
"_grapats" :: "term \<Rightarrow> term \<Rightarrow> term" ("_ | _")
"_grafirst" :: "term \<Rightarrow> term \<Rightarrow> term" ("_ ::= _")
"_grarest" :: "term \<Rightarrow> term \<Rightarrow> term"
"_firsteq" :: "term \<Rightarrow> term \<Rightarrow> term"
"_resteq" :: "term \<Rightarrow> term \<Rightarrow> term"
translations
"_grapats (_firsteq all) (_grarest (CONST grammar_imp rest1 rest2))" <= "CONST grammar_imp all (CONST grammar_imp rest1 rest2)"
"_grapats (_resteq all) (_grarest (CONST grammar_imp rest1 rest2))" <= "_grarest (CONST grammar_imp all (CONST grammar_imp rest1 rest2))"
"_resteq all" <= "_grarest (CONST grammar_imp all rest)"
"_resteq all" <= "_resteq (CONST grammar_imp all rest)"
"_firsteq all" <= "_firsteq (CONST grammar_imp all rest)"
"_firsteq imp" <= "_firsteq (ALL x. imp)"
"_resteq imp" <= "_resteq (ALL x. imp)"
"_grafirst x t" <= "_firsteq (x = t)"
"t" <= "_resteq (x = t)"
This does require the lemma to be internalized, e.g.:
lemma tmp:
"(∀ var. y = Var var ⟶ P) ⟶
(∀ exp var. y = App exp var ⟶ P) ⟶
(∀ assn exp. y = Terms.Let assn exp ⟶ P) ⟶
(∀ var exp. y = Lam [var].exp ⟶ P) ⟶ P"
by (metis exp_assn.exhaust(1))
but then
thm (Grammar) tmp[no_vars]
prints
y ::= Var var | App exp var | Terms.Let assn exp | Lam [var].
exp
which is nice.
It seems that translations work independent of the current mode. That is
why I introduced a mode-dependent abbreviation for the outermost symbol
of the theorem (op ⟶), to make sure my translations only affect the
output in this particular mode. The abbreviation command did however not
work with Trueprop or ==> – how can I adjust this setup to work with the
meta logic directives directly?
There might be more eleganter and saner ways to achieve this. If so,
please let me know.
Thanks,
Joachim
signature.asc
Last updated: Apr 19 2024 at 12:27 UTC