Re: [isabelle] rep_thm



Sean McLaughlin wrote:
  I'm having trouble examining proof terms from the Isabelle top level.
Any nontrivial proof seems to crash both polyml and smlnj.
[...]

ML {* val {prop, der=(_, prf), sign, ...} =
  rep_thm (thm "less_max_iff_disj") *}

This is only 50K lines in the xml output (one tag per line), so it doesn't seem like it should be a memory problem.

Hello Sean,

this is most likely a problem with the ML top level pretty printer.
Note that note that a proof term of a theorem also contains (through
the PThm constructor) the proof terms of all theorems used in the proof
of this theorem. This means that the "prf" above can get quite large,
which can cause ML's pretty printer to crash. If you want to examine
a proof term, better use the Isar commands prf and full_prf (see section
3.3.1 of the Isabelle/Isar Reference Manual), or the printing functions
provided by structure ProofSyntax (see section 5.4.2 of the Isabelle
Reference Manual). These commands produce much more readable output
than ML's pretty printer. Before issuing a command like the
"val ... = rep_thm ..." above, make sure that the print depth of the
ML top level is set to a small value, e.g. by executing the command

ML {* print_depth 0 *}

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe






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