Re: [isabelle] Document preparation question



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"} at {text "::"} at {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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.